proposition: Lemma f_pres_ap_zero : forall x : R1, x[#][0] -> f x[#][0].
proof: Proof. intros. apply ap_wdr_unfolded with (y := f [0]). apply f_pres_apartness with (y := [0]:R1). assumption. assumption. apply f_pres_One. assumption. Qed.
imports: CoRN.reals.CReals