proposition: Lemma Nwmul_ok : forall x y, gen_phiNword (Nwmul x y) == gen_phiNword x * gen_phiNword y.
proof: Proof. intros x; induction x as [|a x IHx]; intros. - norm. - destruct a. + simpl Nwmul. rewrite Nwopp_ok. rewrite IHx. rewrite gen_phiNword_cons. norm. + simpl Nwmul. unfold Nwsub. rewrite Nwadd_ok. rewrite Nwscal_ok. rewrite Nwopp_ok. rewrite IHx. rewrite gen_phiNword_cons. norm. Qed.
imports: Zbool BinInt BinNat Setoid Ring_theory Ring_polynom