proposition: Lemma size_comp s : is_comp s -> size s <= sumn s.
proof: Proof. rewrite /is_comp; elim: s => [//= | [|s0] s IHs] //. rewrite negb_or /= => /IHs/leq_ltn_trans; apply. by rewrite addSnnS; apply leq_addl. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass sorted partition subseq ordtype