proposition: Lemma AbsSmall_e : forall e x : IR, AbsSmall e x -> [0] [<=] e.
proof: Proof. intros. red in H. cut ( [--]e [<=] e). 2: inversion_clear H; apply leEq_transitive with x; assumption. intro. apply mult_cancel_leEq with (Two:IR); astepl ZeroR. apply pos_two. rstepr (e[+]e). apply shift_leEq_plus; astepl ( [--]e). assumption. Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq