proposition: Lemma IPR_IPR_2 : forall p : positive, 2 * IPR p = IPR_2 p.
proof: Proof. unfold IPR; intros [p | p |]. - rewrite IPR_2_xI, Rplus_comm, Rmult_plus_distr_l. now rewrite <-(Rmult_1_r 2) at 4. - now rewrite IPR_2_xO. - now rewrite IPR_2_xH, Rmult_1_r. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField