Lemma natmult_commringfrac {X : commring} {S : subabmonoid _} : ∏ n (x : X × S), natmult (X := commringfrac X S) n (setquotpr (eqrelcommringfrac X S) x) = setquotpr (eqrelcommringfrac X S) (natmult (X := X) n (pr1 x) ,, (pr2 x)). Proof. simpl ; intros n x. induction n as [|n IHn]. - apply (iscompsetquotpr (eqrelcommringfrac X S)). apply hinhpr ; simpl. exists (pr2 x). rewrite !(ringmult0x X). reflexivity. - rewrite !natmultS, IHn. apply (iscompsetquotpr (eqrelcommringfrac X S)). apply hinhpr ; simpl. exists (pr2 x) ; simpl. rewrite <- (ringldistr X). rewrite (ringcomm2 X (pr1 (pr2 x))). rewrite !(ringassoc2 X). reflexivity. Qed.
Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.Groups. Require Import UniMath.Algebra.DivisionRig. Require Import UniMath.Algebra.Domains_and_Fields. Require Import UniMath.Algebra.ConstructiveStructures. Require Import UniMath.MoreFoundations.Tactics.