proposition: Lemma eqEfsubset A B : (A == B) = (A `<=` B) && (B `<=` A).
proof: Proof. apply/eqP/andP => [-> //|[/fsubsetP AB /fsubsetP BA]]. by apply/fsetP=> x; apply/idP/idP=> [/AB|/BA]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)