proposition: Lemma fsubsetD A B C : (A `<=` (B `\` C)) = (A `<=` B) && [disjoint A & C]%fset.
proof: Proof. pose D := A `|` B `|` C. have AD : A `<=` D by rewrite /D -fsetUA fsubsetUl. have BD : B `<=` D by rewrite /D fsetUAC fsubsetUr. rewrite -(@subset_fsubE D) //; last first. by rewrite fsubDset (fsubset_trans BD) // fsubsetUr. rewrite fsubD subsetD !subset_fsubE // disjoint_fsub //. by rewrite /D fsetUAC fsubsetUl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)