proposition: Lemma phi_pos1_succ : forall x : positive, phi_pos1 (Pos.succ x) == 1 + phi_pos1 x.
proof: Proof. exact (ARgen_phiPOS_Psucc (SORsetoid sor) ring_ops_wd (Rth_ARth (SORsetoid sor) ring_ops_wd (SORrt sor))). Qed.
imports: OrderedRing RingMicromega ZArith_base InitialRing Setoid ZArithRing