proposition: Lemma partial_sums_pos_incr : ∀ (a : ℕ → ℝ), (∀ n : ℕ, a n ≥ 0)⇒ Un_growing (partial_sums a).
proof: Proof. Take a : (ℕ → ℝ); such that (∀ n : ℕ, a n ≥ 0). We need to show that (for all n : ℕ, partial_sums a n ≤ partial_sums a (S n)). Take n : ℕ. It holds that (a (S n) ≥ 0). It holds that ((partial_sums a n) + a (S n) = partial_sums a (S n)). We conclude that (& partial_sums a n <= (partial_sums a n) + a (S n) = partial_sums a (S n)). Qed.
imports: Coq.Reals.Reals Lra Classical Classical_Pred_Type ClassicalChoice Automation Libs.Analysis.Sequences Notations Tactics