proposition: Lemma isnonzerolinvel (X : ring) (is : isnonzerorig X) (x : X) (x' : multlinvpair X x) : ((pr1 x') != 0).
proof: Proof. intros. apply (negf (maponpaths (λ a : X, a * x))). assert (e := pr2 x'). change (paths (pr1 x' * x) 1) in e. change (neg (paths (pr1 x' * x) (0 * x))). rewrite e. rewrite (ringmult0x X _). apply is. Defined.
imports: UniMath.Algebra.Groups UniMath.Algebra.RigsAndRings