proposition: Lemma gen_phiNword_morph : ring_morph 0 1 radd rmul rsub ropp req NwO NwI Nwadd Nwmul Nwsub Nwopp Nweq_bool gen_phiNword.
proof: Proof. constructor. - reflexivity. - reflexivity. - exact Nwadd_ok. - intros. unfold Nwsub. rewrite Nwadd_ok. rewrite Nwopp_ok. norm. - exact Nwmul_ok. - exact Nwopp_ok. - exact gen_phiNword_ok. Qed.
imports: Zbool BinInt BinNat Setoid Ring_theory Ring_polynom