proposition: 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: 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.
imports: UniMath.Foundations.NaturalNumbers UniMath.Algebra.RigsAndRings UniMath.Algebra.Groups UniMath.Algebra.DivisionRig UniMath.Algebra.Domains_and_Fields UniMath.Algebra.ConstructiveStructures UniMath.MoreFoundations.Tactics