proposition: Lemma gen_phiZ_add : forall x y, [x + y] == [x] + [y].
proof: Proof. intros x y; repeat rewrite same_genZ; generalize x y;clear x y. induction x;destruct y;simpl;norm. - apply ARgen_phiPOS_add. - apply gen_phiZ1_add_pos_neg. - rewrite gen_phiZ1_add_pos_neg. rewrite ring_add_comm. reflexivity. - rewrite ARgen_phiPOS_add. rewrite ring_opp_add. reflexivity. Qed.
imports: ZArith_base Zpow_def BinInt BinNat Setoid BinList BinPos BinNat BinInt Setoid Ncring Ncring_polynom