proposition: Lemma inj_Q_AbsSmall : forall q1 q2, AbsSmall q1 q2 -> AbsSmall (inj_Q q1) (inj_Q q2).
proof: Proof. intros. red in |- *. elim H. intros. split. astepl (inj_Q [--]q1). apply inj_Q_leEq. assumption. apply inj_Q_leEq. 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