proposition: Lemma AbsSmall_subinterval : forall a b x y : OF, (a[<=]x) -> (a[<=]y) -> (x[<=]b) -> (y[<=]b) -> AbsSmall (b[-]a) (x[-]y).
proof: Proof. intros. split. rstepl (a[+][--]b). rstepr (x[+][--]y). apply plus_resp_leEq_both. assumption. apply inv_resp_leEq. assumption. rstepl (x[+][--]y). rstepr (b[+][--]a). apply plus_resp_leEq_both. assumption. apply inv_resp_leEq. assumption. Qed.
imports: CoRN.reals.Q_in_CReals