proposition: Lemma inj_Q_ap : forall q1 q2, (q1 [#] q2) -> inj_Q q1 [#] inj_Q q2.
proof: Proof. intros q1 q2 H. destruct (ap_imp_less _ _ _ H); [apply less_imp_ap|apply Greater_imp_ap]; apply inj_Q_less; 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