proposition: Lemma mult_IPR : forall p q:positive, IPR (p * q) = IPR p * IPR q.
proof: Proof. intros p q; induction q as [| q IH] using Pos.peano_ind. - now rewrite Pos.mul_1_r, IPR_xH, Rmult_1_r. - now rewrite Pos.mul_succ_r, succ_IPR, plus_IPR, IH, Rmult_plus_distr_l, Rmult_1_r. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField