Lemma isnonzerofromrinvel (X : ring) (is : isnonzerorig X) (x : X) (x' : multrinvpair X x) : x != 0. Proof. intros. apply (negf (maponpaths (λ a : X, a * (pr1 x')))). assert (e := pr2 x'). change (x * pr1 x' = 1) in e. change (x * pr1 x' != 0 * pr1 x'). rewrite e. rewrite (ringmult0x X _). apply is. Defined.
Require Import UniMath.Algebra.Groups.