proposition: Lemma gen_phiNword_Nwcons : forall w n, gen_phiNword (Nwcons n w) == gen_phiN rO rI radd rmul n - gen_phiNword w.
proof: Proof. intros w; destruct w; intros n0. - destruct n0; norm. - unfold Nwcons. rewrite gen_phiNword_cons. reflexivity. Qed.
imports: Zbool BinInt BinNat Setoid Ring_theory Ring_polynom