proposition: Lemma f_pres_inv : forall (x : R1) (H : x[#][0]), f ([1][/] x[//]H)[=]([1][/] f x[//]f_pres_ap_zero x H).
proof: Proof. intros. apply mult_cancel_lft with (z := f x). apply f_pres_ap_zero. assumption. rstepr ([1]:R2). astepr (f [1]). astepl (f (x[*]([1][/] x[//]H))). apply eq_symmetric_unfolded. apply f_well_def. rational. apply f_pres_one. Qed.
imports: CoRN.reals.CReals