proposition: Lemma subset_fsubE C A B : A `<=` C -> B `<=` C -> (fsub C A \subset fsub C B) = (A `<=` B).
proof: Proof. move=> sAC sBC; apply/subsetP/fsubsetP => sAB a; last first. by rewrite !inE => /sAB. by move=> aA; have := sAB _ (fincl_fsub sAC [` aA]); rewrite inE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)