proposition: Lemma Fsub_mono : {homo Fsub : X Y / X \subset Y}.
proof: Proof. move=> X Y subXY; apply: subset_fsub; last by apply/F_bound/fset_sub_val. by apply/F_mono/subset_imfset/subsetP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)