proposition: Lemma fset_fsub X : X `<=` U -> [fsetval x in fsub U X] = X.
proof: Proof. move=> XU; apply/fsetP => x; apply/in_fset_valP/idP. by move=> [xU/=]; rewrite in_fsub. by move=> xX; exists (fsubsetP XU x xX); rewrite /= in_fsub. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)