proposition: Lemma mult_INR : forall n m:nat, INR (n * m) = INR n * INR m.
proof: Proof. intros n m; induction m as [| m IH]. - now rewrite Nat.mul_0_r, INR_0, Rmult_0_r. - now rewrite Nat.mul_succ_r, S_INR, plus_INR, IH, Rmult_plus_distr_l, Rmult_1_r. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField