Lemma afldinvertibletoazero ( A : afld ) ( a : A ) ( p : multinvpair A a ) : a # 0. 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.
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.Domains_and_Fields. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.Algebra.Monoids.