proposition: Lemma fsubset_cardP A B : #|` A| = #|` B| -> reflect (A =i B) (A `<=` B).
proof: Proof. move=> eq_cardAB; apply: (iffP idP) => [/eqVfproper [->//|]|/fsetP -> //]. by rewrite fproperEcard eq_cardAB ltnn andbF. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)