proposition: Lemma inj_Q_inv : forall q1, inj_Q [--]q1 [=] [--](inj_Q q1).
proof: Proof. intro. apply cg_cancel_lft with (x := inj_Q q1). astepr (inj_Q (q1[+][--]q1)). apply eq_symmetric_unfolded. apply inj_Q_plus. astepr (inj_Q [0]). apply inj_Q_wd. algebra. simpl in |- *. rstepl ([0]:R1). 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