proposition: Lemma f_well_def : forall x y : R1, x[=]y -> f x[=]f y.
proof: Proof. intros. apply not_ap_imp_eq. intro. cut (Not (x[#]y)). intro H2. apply H2. red in H1. apply H1. assumption. apply eq_imp_not_ap. assumption. Qed.
imports: CoRN.reals.CReals