proposition: Lemma subIset A B C : (B \subset A) || (C \subset A) -> (B :&: C \subset A).
proof: Proof. by case/orP; apply: subset_trans; rewrite (subsetIl, subsetIr). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)