proposition: Lemma enum_compn_rec_any aux1 aux2 n : n <= aux1 -> n <= aux2 -> enum_compn_rec aux1 n = enum_compn_rec aux2 n.
proof: Proof. elim: aux1 aux2 n => [| aux1 IHaux1] aux2 n /=. by rewrite leqn0 => /eqP -> //=; case aux2. case: (n =P 0) => [-> | /eqP Hn Haux1] //=; first by case aux2. case: aux2 => [| aux2 /= Haux2]. by rewrite leqn0 => /eqP H; rewrite H eq_refl in Hn. rewrite (negbTE Hn); congr flatten; apply eq_in_map => i. rewrite mem_iota add1n ltnS => /andP[Hi _]. congr map; apply: IHaux1; rewrite leq_subLR. - by apply: (leq_trans Haux1); rewrite -{1}(add0n aux1) ltn_add2r. - by apply: (leq_trans Haux2); rewrite -{1}(add0n aux2) ltn_add2r. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass sorted partition subseq ordtype