proposition: Lemma subset_fsub A B C : A `<=` B -> B `<=` C -> fsub C A \subset fsub C B.
proof: Proof. by move=> sAB sBC; rewrite subset_fsubE // (fsubset_trans sAB). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)