proposition: Lemma plus_IPR : forall p q, IPR (p + q) = IPR p + IPR q.
proof: Proof. intros p q; induction q as [| q IH] using Pos.peano_ind. - now rewrite Pos.add_1_r, succ_IPR, Rplus_comm. - rewrite Pos.add_succ_r, 2succ_IPR, IH. now rewrite <-Rplus_assoc, (Rplus_comm (IPR 1)), Rplus_assoc. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField