proposition: Lemma fdisjointWl A B C : A `<=` B -> [disjoint B & C] -> [disjoint A & C].
proof: Proof. move=> AsubB; rewrite -!(@disjoint_fsub (B `|` C)) ?fsetSU //. by apply: disjointWl; rewrite subset_fsub. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)