proposition: Lemma gen_phiZ_morph : ring_morph 0 1 radd rmul rsub ropp req Z0 (Zpos xH) Z.add Z.mul Z.sub Z.opp Zeq_bool gen_phiZ.
proof: Proof. assert ( SRmorph : semi_morph 0 1 radd rmul req Z0 (Zpos xH) Z.add Z.mul Zeq_bool gen_phiZ). - apply mkRmorph;simpl;try rrefl. + apply gen_phiZ_add. + apply gen_phiZ_mul. + apply gen_Zeqb_ok. - apply (Smorph_morph Rsth Reqe Rth Zth SRmorph gen_phiZ_ext). Qed.
imports: Zbool BinInt BinNat Setoid Ring_theory Ring_polynom