proposition: Lemma afldinvertibletoazero ( A : afld ) ( a : A ) ( p : multinvpair A a ) : a # 0.
proof: Proof. intros. destruct p as [ a' p ]. assert ( a' * a # 0 ) as q. { change ( a' * a # 0 ). assert ( a' * a = a * a' ) as f by apply ( ringcomm2 A ). assert ( a * a' = 1 ) as g by apply (pr2 p). rewrite f, g. apply (pr2 A). } assert ( a' * a # a' * ( ringunel1 ( X := A ) ) ) as q'. { assert ( ringunel1 ( X := A ) = a' * ( ringunel1 ( X := A ) ) ) as f. { apply pathsinv0. apply ( ringmultx0 A ). } rewrite <- f. assumption. } apply ( pr1 ( acommring_amult A ) a' ). assumption. Defined.
imports: UniMath.Tactics.EnsureStructuredProofs UniMath.Foundations.PartA UniMath.Foundations.Propositions UniMath.Foundations.NaturalNumbers UniMath.Algebra.RigsAndRings UniMath.Algebra.Domains_and_Fields UniMath.NumberSystems.Integers UniMath.Algebra.Monoids