(R : Ring) : (cring_Z : Ring) $-> R. Proof. snrapply Build_RingHomomorphism. 1: exact (rng_int_mult R 1). repeat split. 1,2: exact _. apply rng_plus_zero_r. Defined.
Require Import Classes.interfaces.canonical_names. Require Import Algebra.AbGroups. Require Import Algebra.Rings.CRing. Require Import Spaces.Int Spaces.Pos. Require Import WildCat.Core.