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