proposition: Lemma IPR_xI : forall p : positive, IPR (p~1) = 2 * IPR p + 1.
proof: Proof. intros p. apply (Rmult_eq_reg_l 2); cycle 1. { apply not_eq_sym, Rlt_not_eq, Rlt_0_2. } now rewrite 2IPR_IPR_2, IPR_2_xI, Rmult_plus_distr_l, Rmult_1_r. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField