proposition: Lemma ARgen_phiPOS_add : forall x y, gen_phiPOS1 (x + y) == (gen_phiPOS1 x) + (gen_phiPOS1 y).
proof: Proof. induction x;destruct y;simpl;norm. - rewrite Pos.add_carry_spec. rewrite ARgen_phiPOS_Psucc. rewrite IHx;norm. add_push (gen_phiPOS1 y);add_push 1;reflexivity. - rewrite IHx;norm;add_push (gen_phiPOS1 y);reflexivity. - rewrite ARgen_phiPOS_Psucc;norm;add_push 1;reflexivity. - rewrite IHx;norm;add_push(gen_phiPOS1 y); add_push 1;reflexivity. - rewrite IHx;norm;add_push(gen_phiPOS1 y);reflexivity. - add_push 1;reflexivity. - rewrite ARgen_phiPOS_Psucc;norm;add_push 1;reflexivity. Qed.
imports: ZArith_base Zpow_def BinInt BinNat Setoid BinList BinPos BinNat BinInt Setoid Ncring Ncring_polynom