Definition afldfracmultinvint ( ab : A × aintdomazerosubmonoid A ) ( is : afldfracapartrelpre ab ( make_dirprod ( @ringunel1 A ) ( unel ( aintdomazerosubmonoid A ) ) ) ) : A × aintdomazerosubmonoid A. Proof. intros. destruct ab as [ a b ]. destruct b as [ b b' ]. split with b. simpl in is. split with a. unfold afldfracapartrelpre in is. simpl in is. change ( a # 0 ). rewrite ( @ringmult0x A ) in is. rewrite ( @ringrunax2 A ) in is. assumption. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.Domains_and_Fields.