proposition: Lemma gen_phiN_morph : ring_morph 0 1 radd rmul rsub ropp req 0%N 1%N N.add N.mul Nsub Nopp N.eqb gen_phiN.
proof: Proof. constructor; simpl; try reflexivity. - apply gen_phiN_add. - apply gen_phiN_sub. - apply gen_phiN_mult. - intros x y EQ. apply N.eqb_eq in EQ. now subst. Qed.
imports: Zbool BinInt BinNat Setoid Ring_theory Ring_polynom