proposition: Lemma gen_phiNword_ok : forall w1 w2, Nweq_bool w1 w2 = true -> gen_phiNword w1 == gen_phiNword w2.
proof: Proof. intros w1; induction w1 as [|a w1 IHw1]; intros w2 H. - simpl. rewrite (gen_phiNword0_ok _ H). reflexivity. - rewrite gen_phiNword_cons. destruct w2 as [|n w2]. + simpl in H. destruct a; try discriminate. rewrite (gen_phiNword0_ok _ H). norm. + simpl in H. rewrite gen_phiNword_cons. case_eq (N.eqb a n); intros H0. * rewrite H0 in H. apply N.eqb_eq in H0. rewrite <- H0. rewrite (IHw1 _ H). reflexivity. * rewrite H0 in H; discriminate H. Qed.
imports: Zbool BinInt BinNat Setoid Ring_theory Ring_polynom