proposition: Lemma gen_phiZ_opp : forall x, [- x] == - [x].
proof: Proof. intros x. repeat rewrite same_genZ. generalize x ;clear x. induction x;simpl;norm. rewrite ring_opp_opp. reflexivity. Qed.
imports: ZArith_base Zpow_def BinInt BinNat Setoid BinList BinPos BinNat BinInt Setoid Ncring Ncring_polynom