proposition: Lemma leEq_inj_Q : forall q1 q2, (inj_Q q1 [<=] inj_Q q2) -> q1 [<=] q2.
proof: Proof. intros. rewrite -> leEq_def; intro. apply less_irreflexive_unfolded with (x := inj_Q q2). eapply less_leEq_trans. 2: apply H. apply inj_Q_less. auto. 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