proposition: Lemma sum_pos_lt n u : (forall i, lt i n -> 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. intros i Hi; apply p. lia. specialize (p O). assert_specialize p by lia. lra. Qed.
imports: Lia Reals Psatz