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