proposition: Lemma AbsSmall_transitive : forall e x y : IR, AbsSmall e x -> AbsIR y [<=] AbsIR x -> AbsSmall e y.
proof: Proof. intros. apply AbsIR_imp_AbsSmall. eapply leEq_transitive. apply H0. apply AbsSmall_imp_AbsIR; assumption. Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq