proposition: Lemma fsubDset A B C : (A `\` B `<=` C) = (A `<=` B `|` C).
proof: Proof. apply/fsubsetP/fsubsetP=> sABC x; rewrite !inE. by case Bx: (x \in B) => // Ax; rewrite sABC ?in_fsetD ?Bx. by case Bx: (x \in B) => //; move/sABC; rewrite inE Bx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)