proposition: Lemma sumn_sort l S : sumn (sort S l) = sumn l.
proof: Proof. Proof using. by have:= perm_sort S l => /permPl/perm_sumn. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(finset bigop path binomial)