proposition: Lemma ptsum_homo x y : (x <= y)%N -> (\sum_(i < x) S i <= \sum_(i < y) S i).
proof: Proof. move=> le_xy; rewrite -!(big_mkord predT) -(subnKC le_xy) /=. by rewrite /index_iota !subn0 iotaD big_cat /= lerDl sumr_ge0. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology