proposition: Lemma ger_big_ord_psum n : \sum_(i < n) `|S i| <= psum S.
proof: Proof. rewrite -(big_mkord predT (fun i => `|S i|)) /=. by apply/ger_big_psum => //; rewrite iota_uniq. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology