proposition: Lemma enum_compn_any aux n : n <= aux -> enum_compn_rec aux n = enum_compn n.
proof: Proof. by rewrite /enum_compn => Hn; apply enum_compn_rec_any. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass sorted partition subseq ordtype