proposition: Lemma map_pres_ap_zero : forall (f : Homomorphism) (x : R1), x[#][0] -> f x[#][0].
proof: Proof. intros. rename X into H. apply ap_wdr_unfolded with (y := f [0]). apply map_pres_apartness with (y := [0]:R1). exact H. apply map_pres_zero_unfolded. Qed.
imports: CoRN.reals.CReals