proposition: Lemma minus_INR : forall n m, (m <= n)%nat -> INR (n - m) = INR n - INR m.
proof: Proof. intros n m le; induction le as [|n' H' IH]. - now rewrite Nat.sub_diag, Rminus_diag. - rewrite Nat.sub_succ_l by assumption. now rewrite 2S_INR, IH, Rplus_minus_swap. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField