proposition: Lemma gen_phiNword0_ok : forall w, Nw_is0 w = true -> gen_phiNword w == 0.
proof: Proof. intros w; induction w as [|a w IHw]; simpl; intros; auto. - reflexivity. - destruct a. + destruct w. * reflexivity. * rewrite IHw; trivial. apply (ARopp_zero Rsth Reqe ARth). + discriminate. Qed.
imports: Zbool BinInt BinNat Setoid Ring_theory Ring_polynom