proposition: Lemma Nwopp_ok : forall x, gen_phiNword (Nwopp x) == - gen_phiNword x.
proof: Proof. simpl. unfold Nwopp; simpl. intros. rewrite gen_phiNword_Nwcons; norm. Qed.
imports: Zbool BinInt BinNat Setoid Ring_theory Ring_polynom