proposition: Lemma minus_IPR : forall p q, (q < p)%positive -> IPR (p - q) = IPR p - IPR q.
proof: Proof. induction p as [| p IH] using Pos.peano_ind. - now intros q H%Pos.nlt_1_r. - intros q H; destruct q as [| q] using Pos.peano_ind. + now rewrite succ_IPR, <-Pos.add_1_r, Pos.add_sub, IPR_xH, Rplus_minus_l. + rewrite 2succ_IPR, IPR_xH, Rminus_plus_l_l. rewrite <-2Pos.add_1_r, (Pos.add_comm q). rewrite Pos.sub_add_distr by (now rewrite Pos.add_1_l, Pos.add_1_r). now rewrite Pos.add_sub, IH by (now apply Pos.succ_lt_mono). Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField