proposition: Lemma inj_Q_strext : forall q1 q2, (inj_Q q1 [#] inj_Q q2) -> q1 [#] q2.
proof: Proof. intros q1 q2. generalize (den_is_nonzero q1). generalize (den_is_nonzero q2). case q1. intros n1 d1. case q2. intros n2 d2. intros H H0 H1. simpl in |- *. simpl in H. simpl in H0. unfold Qap in |- *. unfold Qeq in |- *. unfold Qnum in |- *. unfold Qden in |- *. intro. cut (~ (inj_Q (Qmake n1 d1) [=] inj_Q (Qmake n2 d2))). intro. elim H3. simpl in |- *. apply mult_cancel_lft with (z := nring (R:=R1) d1[*]nring (R:=R1) d2). apply mult_resp_ap_zero. assumption. assumption. rstepl (zring (R:=R1) n1[*]nring (R:=R1) d2). rstepr (zring (R:=R1) n2[*]nring (R:=R1) d1). astepr (zring (R:=R1) (n1 * d2)). astepr (zring (R:=R1) n1[*]zring (R:=R1) d2). apply mult_wdr. astepl (zring (R:=R1) (Z_of_nat (nat_of_P d2))). rewrite inject_nat_convert. algebra. rewrite H2. astepl (zring (R:=R1) n2[*]zring (R:=R1) d1). apply mult_wdr. astepr (zring (R:=R1) (Z_of_nat (nat_of_P d1))). rewrite inject_nat_convert. algebra. change (inj_Q (Qmake n1 d1)[~=]inj_Q (Qmake n2 d2)) in |- *. apply ap_imp_neq. assumption. 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