proposition: Lemma fsubE A B (AsubB : A `<=` B) : fsub B A = [set fincl AsubB x | x : A].
proof: Proof. apply/setP => x; rewrite in_set; apply/idP/imsetP => [|[[a aA] aA' ->]] //. by move=> xA; exists [` xA]=> //; apply: val_inj. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)