Definition afldfracmultinv ( a : afldfrac0 ) ( is : a # 0 ) : multinvpair afldfrac0 a. Proof. intros. assert ( forall b : afldfrac0, isaprop ( b # 0 -> multinvpair afldfrac0 b ) ) as int. { intros. apply impred. intro p. apply ( isapropmultinvpair afldfrac0 ). } assert ( forall b : afldfrac0, b # 0 -> multinvpair afldfrac0 b ) as p. { apply ( setquotunivprop _ ( fun x0 => make_hProp _ ( int x0 ) ) ). intros bc q. destruct bc as [ b c ]. assert ( afldfracapartrelpre ( make_dirprod b c ) ( make_dirprod ( @ringunel1 A ) ( unel (aintdomazerosubmonoid A ) ) ) ) as is' by apply q. split with (setquotpr (eqrelcommringfrac A (aintdomazerosubmonoid A)) (afldfracmultinvint ( make_dirprod b c ) is' ) ). split. - change ( setquotpr ( eqrelcommringfrac A ( aintdomazerosubmonoid A ) ) ( make_dirprod ( @op2 A ( pr1 ( afldfracmultinvint ( make_dirprod b c ) is' ) ) b ) ( @op ( aintdomazerosubmonoid A ) ( pr2 ( afldfracmultinvint ( make_dirprod b c ) is' ) ) c ) ) = ( commringfracunel2 A ( aintdomazerosubmonoid A ) ) ). apply iscompsetquotpr. unfold commringfracunel2int. destruct c as [ c c' ]. simpl. apply total2tohexists. split with ( make_carrier ( fun x : pr1 A => x # 0 ) 1 ( pr1 ( pr2 A ) ) ). simpl. rewrite 3! ( @ringrunax2 A ). rewrite ( @ringlunax2 A ). apply ( @ringcomm2 A ). - change ( setquotpr ( eqrelcommringfrac A ( aintdomazerosubmonoid A ) ) ( make_dirprod ( @op2 A b ( pr1 ( afldfracmultinvint ( make_dirprod b c ) is' ) ) ) ( @op ( aintdomazerosubmonoid A ) c ( pr2 ( afldfracmultinvint ( make_dirprod b c ) is' ) ) ) ) = ( commringfracunel2 A ( aintdomazerosubmonoid A ) ) ). apply iscompsetquotpr. destruct c as [ c c' ]. simpl. apply total2tohexists. split with ( make_carrier ( fun x : pr1 A => x # 0 ) 1 ( pr1 ( pr2 A ) ) ). simpl. rewrite 3! ( @ringrunax2 A ). rewrite ( @ringlunax2 A ). apply ( @ringcomm2 A ). } apply p. assumption. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.Domains_and_Fields.