proposition: Lemma AbsSmall_intermediate : forall x y z eps : R, x [<=] y -> y [<=] z -> AbsSmall eps (z[-]x) -> AbsSmall eps (z[-]y).
proof: Proof. intros. apply leEq_imp_AbsSmall. apply shift_leEq_minus; astepl y. assumption. unfold AbsSmall in H1. elim H1; intros. apply leEq_transitive with (z[-]x); try assumption. apply minus_resp_leEq_rht. assumption. Qed.
imports: CoRN.algebra.COrdFields2