proposition: Lemma fproperIset A B C : (B `<` A) || (C `<` A) -> (B `&` C `<` A).
proof: Proof. by case/orP; apply: fsub_proper_trans; rewrite (fsubsetIl, fsubsetIr). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)