proposition: Lemma sigma_split_v2 : ∀ (a : ℕ → ℝ) (k l N : ℕ), (k < l)%nat ⇒ (l ≤ N)%nat ⇒ sigma a k N = sigma a k (l - 1)%nat + sigma a l N.
proof: Proof. Take a : (ℕ → ℝ) and k, l, Nn : ℕ; such that (k < l)%nat and (l ≤ Nn)%nat. It holds that (l = S (l - 1)%nat) (i). rewrite (i) at 2. By sigma_split it suffices to show that (k <= l - 1 < Nn)%nat. We show both (k <= l - 1)%nat and (l - 1 < Nn)%nat. - We conclude that (k ≤ l - 1)%nat. - We conclude that (l - 1 < Nn)%nat. Qed.
imports: Coq.Reals.Reals Lra Classical Classical_Pred_Type ClassicalChoice Automation Libs.Analysis.Sequences Notations Tactics