proposition: Lemma isarchcommringfrac {X : commring} {S : subabmonoid _} (R : hrel X) Hop1 Hop2 Hs: R 1%ring 0%ring -> istrans R -> isarchring R -> isarchring (X := commringfrac X S) (commringfracgt X S (R := R) Hop1 Hop2 Hs).
proof: Proof. intros H0 Htra Hr. split. - simple refine (setquotunivprop _ (λ _, (_,,_)) _). apply isapropimpl, propproperty. intros x Hx. revert Hx ; apply hinhuniv ; intros (c,Hx) ; simpl in Hx. rewrite !(ringmult0x X), (ringrunax2 X) in Hx. apply (hinhfun (X := ∑ n, commringfracgt X S Hop1 Hop2 Hs (setquotpr (eqrelcommringfrac X S) ((nattoring n * pr1 x)%ring,, pr2 x)) 1%ring)). intros H. eexists (pr1 H). unfold nattoring. rewrite (nattorig_natmult (X := commringfrac X S)). rewrite (natmult_commringfrac (X := X) (S := S)). rewrite <- (nattorig_natmult (X := X)). now apply (pr2 H). generalize (isarchring_1 _ Hr _ Hx) (isarchring_2 _ Hr (pr1 (pr2 x) * pr1 c)%ring). apply hinhfun2. intros (m,Hm) (n,Hn). exists (max 1 n * m)%nat. destruct n ; simpl max. + apply hinhpr ; simpl. exists c. rewrite (ringrunax2 X), (ringlunax2 X), (ringassoc2 X). eapply Htra. exact Hm. eapply Htra. exact H0. exact Hn. + unfold nattoring. rewrite (nattorig_natmult (X := X)), natmult_mult. apply hinhpr ; simpl. exists c. change (R (natmult (succ n) (natmult (X := X) m (pr1 x)) * 1 * pr1 c)%ring (1 * pr1 (pr2 x) * pr1 c)%ring). rewrite <- (nattorig_natmult (X := X)), (ringrunax2 X), (ringlunax2 X), (ringassoc2 X), (nattorig_natmult (X := X)). eapply Htra. apply (natmult_binophrel (X := X) R). exact Htra. exact Hop1. rewrite <- (nattorig_natmult (X := X)), (ringassoc2 X). exact Hm. exact Hn. - simple refine (setquotunivprop _ _ _). intros x. apply (hinhfun (X := ∑ n : nat, commringfracgt X S Hop1 Hop2 Hs (setquotpr (eqrelcommringfrac X S) (nattoring n,, unel S)) (setquotpr (eqrelcommringfrac X S) x))). intros (n,Hn). exists n. unfold nattoring, nattorig. change 1%rig with (setquotpr (eqrelcommringfrac X S) (1%ring,, unel S)). rewrite (natmult_commringfrac (X := X) (S := S) n). exact Hn. generalize (isarchring_1 _ Hr _ (Hs (pr1 (pr2 x)) (pr2 (pr2 x)))) (isarchring_2 _ Hr (pr1 x)%ring). apply hinhfun2. intros (m,Hm) (n,Hn). exists (max 1 n * m)%nat. destruct n ; simpl max. + apply hinhpr ; simpl. exists (pr2 x). apply (isringmultgttoisrringmultgt X). exact Hop1. exact Hop2. apply Hs. apply (pr2 (pr2 x)). eapply Htra. exact Hm. eapply Htra. exact H0. rewrite (ringrunax2 X). exact Hn. + apply hinhpr ; simpl. exists (pr2 x). change (n * m + m)%nat with (succ n * m)%nat. unfold nattoring. apply (isringmultgttoisrringmultgt X). exact Hop1. exact Hop2. apply Hs. apply (pr2 (pr2 x)). rewrite (ringrunax2 X), (nattorig_natmult (X := X)), natmult_mult. eapply Htra. apply (natmult_binophrel (X := X) R). exact Htra. exact Hop1. rewrite <- (nattorig_natmult (X := X)). exact Hm. exact Hn. Qed.
imports: UniMath.Foundations.NaturalNumbers UniMath.Algebra.RigsAndRings UniMath.Algebra.Groups UniMath.Algebra.DivisionRig UniMath.Algebra.Domains_and_Fields UniMath.Algebra.ConstructiveStructures UniMath.MoreFoundations.Tactics