proposition: Lemma map_pres_apartness : forall (f : Homomorphism) (x y : R1), x[#]y -> f x[#]f y.
proof: Proof. intros f x y H. cut (x[<]y or y[<]x). intro H0. case H0. intro. apply less_imp_ap. apply map_pres_less_unfolded. assumption. intro H1. apply Greater_imp_ap. apply map_pres_less_unfolded. exact H1. apply ap_imp_less. exact H. Qed.
imports: CoRN.reals.CReals