proposition: Lemma fsub_inj B : {in [pred A | A `<=` B] &, injective (fsub B)}.
proof: Proof. move=> A A'; rewrite -!topredE /= => sAB sA'B /setP eqAA'; apply/fsetP => a. apply/idP/idP => mem_a. by have := eqAA' (fincl sAB [` mem_a]); rewrite !inE // => <-. by have := eqAA' (fincl sA'B [` mem_a]); rewrite !inE // => ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)