proposition: Lemma fsub_proper_trans B A C : A `<=` B -> B `<` C -> A `<` C.
proof: Proof. rewrite !fproperEcard => sAB /andP [sBC lt_BC]. by rewrite (fsubset_trans sAB) //= (leq_ltn_trans _ lt_BC) // fsubset_leq_card. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)