proposition: Fact rowcompnP d : is_comp_of_n d (rowcomp d).
proof: Proof. by case: d => [//= | d]; rewrite /is_comp_of_n /= addn0 eq_refl. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass sorted partition subseq ordtype