proposition: Lemma f_pres_One : f [0][=][0].
proof: Proof. intros. apply cg_cancel_lft with (x := f [0]). astepr (f [0]). astepl (f ([0][+][0])). apply eq_symmetric_unfolded. red in H3. apply f_well_def. algebra. Qed.
imports: CoRN.reals.CReals