proposition: Lemma fsubUset X Y Z : (X `|` Y `<=` Z) = (X `<=` Z) && (Y `<=` Z).
proof: Proof. apply/idP/andP => [H | [H1 H2]]. - by split; apply: sub_trans _ H; rewrite ?fsubUl ?fsubUr. - apply/subP => x. rewrite in_fset; case/orP; move: x; exact/subP. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)