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