proposition: Lemma card_geqP {A n} : reflect (exists s, [/\ uniq s, size s = n & {subset s <= A}]) (n <= #|A|).
proof: Proof. apply: (iffP idP) => [n_le_A|[s] [uniq_s size_s /subsetP subA]]; last first. by rewrite -size_s -(card_uniqP _ uniq_s); exact: subset_leq_card. exists (take n (enum A)); rewrite take_uniq ?enum_uniq // size_take. split => //; last by move => x /mem_take; rewrite mem_enum. case: (ltnP n (size (enum A))) => // size_A. by apply/eqP; rewrite eqn_leq size_A -cardE n_le_A. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)