proposition: Lemma map_pres_zero : forall f : Homomorphism, f (cm_unit R1)[=]cm_unit R2.
proof: Proof. intros. apply cg_cancel_lft with (x := f [0]). apply eq_transitive_unfolded with (f [0]). apply eq_transitive_unfolded with (f ([0][+][0])). apply eq_symmetric_unfolded. apply map_pres_plus_unfolded. apply map_wd_unfolded with (f := f). algebra. algebra. Qed.
imports: CoRN.reals.CReals