proposition: Lemma subDset A B C : (A :\: B \subset C) = (A \subset B :|: C).
proof: Proof. apply/subsetP/subsetP=> sABC x; rewrite !inE. by case Bx: (x \in B) => // Ax; rewrite sABC ?inE ?Bx. by case Bx: (x \in B) => // /sABC; rewrite inE Bx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)