proposition: Lemma AbsSmall_x_minus_delta : forall x eps delta : R, [0] [<=] eps -> [0] [<=] delta -> delta [<=] eps -> AbsSmall eps (x[-] (x[-]delta)).
proof: Proof. intros. rstepr delta. apply leEq_imp_AbsSmall. assumption. assumption. Qed.
imports: CoRN.algebra.COrdFields2