Definition ringneq0andmultlinv (X : ring) (n m : X) (isnm : ((n * m) != 0)) : n != 0. Proof. intros. intro e. rewrite e in isnm. rewrite (ringmult0x X) in isnm. induction (isnm (idpath _)). Defined.
Require Import UniMath.Algebra.Groups.