proposition: Lemma leq_lmax c : c \in C -> size c <= lmax.
proof: Proof. move=> cC; apply sorted_leq_last. rewrite /l /sort_sizes; exact/sort_sorted/leq_total. rewrite mem_sort; apply/mapP; by exists c. Qed.
imports: mathcomp(all_ssreflect path ssralg ssrnum) ssr_ext