proposition: Lemma inj_Q_mult : forall q1 q2, inj_Q (q1[*]q2) [=] inj_Q q1[*]inj_Q q2.
proof: Proof. intros. generalize (den_is_nonzero q1). generalize (den_is_nonzero q2). case q1. intros n1 d1. case q2. intros n2 d2. simpl in |- *. intros. apply mult_cancel_lft with (z := nring (R:=R1) d1[*]nring (R:=R1) d2). apply mult_resp_ap_zero. assumption. trivial. astepr (zring (R:=R1) (n1 * n2)). astepr (nring (R:=R1) (d1 * d2)%positive[*] (zring (R:=R1) (n1 * n2)[/]nring (R:=R1) (d1 * d2)%positive[//] den_is_nonzero (Qmake (n1 * n2)%Z (d1 * d2)%positive))). apply mult_wdl. rewrite nat_of_P_mult_morphism. algebra. astepr (zring (R:=R1) n1[*]zring (R:=R1) n2). apply zring_mult. rational. Qed.
imports: CoRN.model.reals.Cauchy_IR CoRN.model.monoids.Nmonoid CoRN.model.rings.Zring CoRN.algebra.CRing_Homomorphisms CoRN.algebra.Expon Coq.QArith.Qpower CoRN.tactics.CornTac