proposition: Lemma map_pres_inv_unfolded : forall (f : Homomorphism) (x : R1) (H : x[#][0]), f ([1][/] x[//]H)[=]([1][/] f x[//]map_pres_ap_zero f x H).
proof: Proof. intros. apply mult_cancel_lft with (z := f x). apply map_pres_ap_zero. assumption. rstepr ([1]:R2). astepl (f [1]). apply map_pres_one_unfolded. astepl (f (x[*]([1][/] x[//]H))). apply map_pres_mult_unfolded. apply map_wd_unfolded. rational. Qed.
imports: CoRN.reals.CReals