proposition: Lemma inj_Q_minus : forall q1 q2, inj_Q (q1[-]q2) [=] inj_Q q1[-]inj_Q q2.
proof: Proof. intros. astepl (inj_Q (q1[+][--]q2)). astepr (inj_Q q1[+]inj_Q [--]q2). apply inj_Q_plus. astepr (inj_Q q1[+][--](inj_Q q2)). apply plus_resp_eq. apply inj_Q_inv. 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