proposition: Lemma map_pres_minus : forall f : Homomorphism, fun_pres_un_fun f (cg_inv (c:=R1)) (cg_inv (c:=R2)).
proof: Proof. intro f. red in |- *. intro. apply cg_cancel_lft with (x := f x). astepr ([0]:R2). apply eq_transitive_unfolded with (f (x[+][--]x)). apply eq_symmetric_unfolded. apply map_pres_plus_unfolded. astepl (f [0]). apply map_pres_zero_unfolded. apply map_wd_unfolded. algebra. Qed.
imports: CoRN.reals.CReals