proposition: Lemma ARgen_phiPOS_add : forall x y, gen_phiPOS1 (x + y) == (gen_phiPOS1 x) + (gen_phiPOS1 y).
proof: Proof. intros x;induction x as [x IHx|x IHx|]; intros y;destruct y as [y|y|];simpl;norm. - rewrite Pos.add_carry_spec. rewrite ARgen_phiPOS_Psucc. rewrite IHx;norm. add_push (gen_phiPOS1 y);add_push 1;rrefl. - rewrite IHx;norm;add_push (gen_phiPOS1 y);rrefl. - rewrite ARgen_phiPOS_Psucc;norm;add_push 1;rrefl. - rewrite IHx;norm;add_push(gen_phiPOS1 y); add_push 1;rrefl. - rewrite IHx;norm;add_push(gen_phiPOS1 y);rrefl. - add_push 1;rrefl. - rewrite ARgen_phiPOS_Psucc;norm;add_push 1;rrefl. Qed.
imports: Zbool BinInt BinNat Setoid Ring_theory Ring_polynom