proposition: Lemma map_pres_one : forall f : Homomorphism, f (cr_one R1)[=]cr_one R2.
proof: Proof. intros. apply eq_symmetric_unfolded. apply mult_cancel_lft with (z := f [1]). apply map_pres_ap_zero. apply ring_non_triv. astepl (f [1]). astepl (f ([1][*][1])). apply map_pres_mult_unfolded. apply map_wd_unfolded with (f := f). algebra. Qed.
imports: CoRN.reals.CReals