proposition: Lemma f_pres_one : f [1][=][1].
proof: Proof. intros. apply eq_symmetric_unfolded. apply mult_cancel_lft with (z := f [1]). apply f_pres_ap_zero. apply ring_non_triv. astepl (f [1]). astepr (f ([1][*][1])). apply f_well_def. algebra. Qed.
imports: CoRN.reals.CReals