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