proposition: Lemma cring_morph: ring_morph zero one _+_ _*_ _-_ -_ _==_ 0%Z 1%Z Z.add Z.mul Z.sub Z.opp Zeq_bool Ncring_initial.gen_phiZ.
proof: Proof. intros. apply mkmorph ; intros; simpl; try reflexivity. - rewrite Ncring_initial.gen_phiZ_add; reflexivity. - rewrite ring_sub_def. unfold Z.sub. rewrite Ncring_initial.gen_phiZ_add. rewrite Ncring_initial.gen_phiZ_opp; reflexivity. - rewrite Ncring_initial.gen_phiZ_mul; reflexivity. - rewrite Ncring_initial.gen_phiZ_opp; reflexivity. - rewrite (Zeqb_ok x y H). reflexivity. Defined.
imports: List Setoid BinPos BinList Znumtheory Morphisms Setoid Bool ZArith_base Algebra_syntax Ncring Ncring_initial Ncring_tac InitialRing