proposition: Lemma AbsSmall_inj_Q : forall q e, AbsSmall (inj_Q e) (inj_Q q) -> AbsSmall e q.
proof: Proof. intros. elim H. intros. split. apply leEq_inj_Q. apply leEq_wdl with (x := [--](inj_Q e)). assumption. apply eq_symmetric_unfolded. apply inj_Q_inv. apply leEq_inj_Q. 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