proposition: Lemma fsubK A B : A `<=` B -> [fsetval k in fsub B A] = A.
proof: Proof. move=> AsubB; apply/fsetP => k /=; symmetry. have [kB|kNB] := (boolP (k \in B)). by rewrite in_fset_valT /= inE. by rewrite in_fset_valF //; apply: contraNF kNB; apply/fsubsetP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)