proposition: Lemma inj_Q_less : forall q1 q2, (q1 [<] q2) -> inj_Q q1 [<] inj_Q q2.
proof: Proof. intros q1 q2. case q1. intros n1 d1. case q2. intros n2 d2. intro H. simpl in H. unfold Qlt in H. simpl in H. simpl in |- *. apply mult_cancel_less with (z := nring (R:=R1) d1[*]nring (R:=R1) d2). apply mult_resp_pos. elim (ZL4' d1); intros. rewrite p. apply pos_nring_S. elim (ZL4' d2); intros. rewrite p. apply pos_nring_S. rstepl (zring (R:=R1) n1[*]nring (R:=R1) d2). rstepr (zring (R:=R1) n2[*]nring (R:=R1) d1). apply less_wdl with (x := zring (R:=R1) n1[*]zring (R:=R1) (Z_of_nat d2)). apply less_wdr with (y := zring (R:=R1) n2[*]zring (R:=R1) (Z_of_nat d1)). apply less_wdl with (x := zring (R:=R1) (n1 * d2)). apply less_wdr with (y := zring (R:=R1) (n2 * d1)). apply zring_less. apply CZlt_to. assumption. rewrite inject_nat_convert. apply zring_mult. rewrite inject_nat_convert. apply zring_mult. algebra. algebra. 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