proposition: Lemma ARgen_phiPOS_Psucc : forall x, gen_phiPOS1 (Pos.succ x) == 1 + (gen_phiPOS1 x).
proof: Proof. induction x;rsimpl;norm. rewrite IHx. gen_rewrite. add_push 1. reflexivity. Qed.
imports: ZArith_base Zpow_def BinInt BinNat Setoid BinList BinPos BinNat BinInt Setoid Ncring Ncring_polynom