proposition: Lemma sum_max1 : forall N b f, (forall n, f n >= 0) -> sum_f_R0 f (max N (S b)) >= sum_f_R0 f (S b).
proof: Proof. intros N b f Hpos. assert (H : (S b <= max N (S b))%nat) by intuition. induction H. intuition. rewrite tech5. replace (sum_f_R0 f (S b)) with (sum_f_R0 f (S b) + 0) by ring. apply Rplus_ge_compat. apply IHle. apply Hpos. Qed.
imports: PeanoNat Rseries_facts Rsequence_facts Rsequence_subsequence Rpser_usual Reals Rsequence_tactics Rtactic Lra