proposition: Lemma msubIset A B C : (B `<=` A) || (C `<=` A) -> (B `&` C `<=` A).
proof: Proof. by case/orP; apply: msubset_trans; rewrite (msubsetIl, msubsetIr). Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop tuple) finmap