proposition: Lemma gen_phiZ1_add_pos_neg : forall x y, gen_phiZ1 (Z.pos_sub x y) == gen_phiPOS1 x + -gen_phiPOS1 y.
proof: Proof. intros x y. generalize (Z.pos_sub_discr x y). destruct (Z.pos_sub x y) as [|p|p]; intros; subst. - now rewrite ring_opp_def. - rewrite ARgen_phiPOS_add;simpl;norm. add_push (gen_phiPOS1 p). rewrite ring_opp_def;norm. - rewrite ARgen_phiPOS_add;simpl;norm. rewrite ring_opp_def;norm. Qed.
imports: ZArith_base Zpow_def BinInt BinNat Setoid BinList BinPos BinNat BinInt Setoid Ncring Ncring_polynom