proposition: Lemma f_pres_apartness : forall x y : R1, x[#]y -> f x[#]f y.
proof: Proof. intros. cut (x[<]y or y[<]x). intro H0. case H0. intro. apply less_imp_ap. red in H2. apply H2. assumption. intro. apply Greater_imp_ap. red in H2. apply H2. assumption. apply ap_imp_less. assumption. Qed.
imports: CoRN.reals.CReals