proposition: Lemma succ_IPR : forall p, IPR (Pos.succ p) = IPR 1 + IPR p.
proof: Proof. induction p as [p IH |p IH |]. - simpl; rewrite IPR_xO, IPR_xI, IH, IPR_xH, Rmult_plus_distr_l. now rewrite (Rplus_comm 1), (Rplus_assoc _ 1), Rplus_diag, Rplus_comm. - now simpl; rewrite IPR_xI, IPR_xO, IPR_xH, Rplus_comm. - now simpl; rewrite IPR_xO, <-Rplus_diag. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField