proposition: Lemma less_inj_Q : forall q1 q2, (inj_Q q1 [<] inj_Q q2) -> q1 [<] q2.
proof: Proof. intros. cut (q1 [#] q2). intro H0. case (ap_imp_less _ q1 q2 H0). intro. assumption. intro. exfalso. cut (inj_Q q2 [<] inj_Q q1). change (Not (inj_Q q2 [<] inj_Q q1)) in |- *. apply less_antisymmetric_unfolded. assumption. apply inj_Q_less. assumption. apply inj_Q_strext. apply less_imp_ap. 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