proposition: Lemma inj_Q_plus : 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. assumption. astepr (zring (R:=R1) (n1 * d2 + n2 * d1)). astepr (nring (R:=R1) (d1 * d2)%positive[*] (zring (R:=R1) (n1 * d2 + n2 * d1)[/]nring (R:=R1) (d1 * d2)%positive[//] den_is_nonzero (Qmake (n1 * d2 + n2 * d1)%Z (d1 * d2)%positive))). apply mult_wdl. rewrite nat_of_P_mult_morphism. algebra. astepr (zring (R:=R1) n1[*]nring (R:=R1) d2[+]zring (R:=R1) n2[*]nring (R:=R1) d1). astepl (zring (R:=R1) (n1 * d2)[+]zring (R:=R1) (n2 * d1)). apply bin_op_wd_unfolded. astepr (zring (R:=R1) n1[*]zring (R:=R1) (Z_of_nat (nat_of_P d2))). rewrite inject_nat_convert. algebra. astepr (zring (R:=R1) n2[*]zring (R:=R1) (Z_of_nat (nat_of_P d1))). rewrite inject_nat_convert. algebra. 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