proposition: Lemma IPR_2_xI : forall p : positive, IPR_2 (p~1) = 2 * (IPR_2 p) + 2.
proof: Proof. intros p; simpl. rewrite (Rplus_comm _ 2), <-(Rmult_1_r 2) at 1. now rewrite <-(Rmult_plus_distr_l 2). Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField