proposition: Lemma msubsetU A B C : (A `<=` B) || (A `<=` C) -> A `<=` (B `|` C).
proof: Proof. by move=> /orP [] /msubset_trans ->. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop tuple) finmap