lemma proved term proof

`sumFirst_nonneg`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 107lemma sumFirst_nonneg (m : Nat) (s : Stream) : 0 ≤ sumFirst m s := by

Term-mode proof.

 108  unfold sumFirst
 109  apply Finset.sum_nonneg
 110  intro i _
 111  split
 112  · norm_num
 113  · norm_num
 114

Lean names referenced from this declaration's body.