proposition: Lemma sum_pos n u : (forall i, 0 <= u i) -> 0 <= sum n u.
proof: Proof. revert u; induction n; auto; intros u p; simpl. lra. specialize (IHn (shift 1 u)). assert_specialize IHn. intro; apply p. specialize (p O). lra. Qed.
imports: Lia Reals Psatz