proposition: Lemma fsub_eq0 A B : A `<=` B -> (fsub B A == set0) = (A == fset0).
proof: Proof. by move=> sAB; rewrite -fsub0 (inj_in_eq (@fsub_inj _)) -?topredE /=. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)