proposition: Lemma foldr_maxn s : foldr maxn 0 [seq i.+1 | i <- s] = \max_(i <- s) S i.
proof: Proof. elim: s => [| s0 s IHs] /=; first by rewrite big_nil. by rewrite big_cons IHs. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass partition