proposition: Lemma disjoint_fsub C A B : A `|` B `<=` C -> [disjoint fsub C A & fsub C B]%bool = [disjoint A & B].
proof: Proof. move=> ABsubC. apply/idP/idP=> [/pred0P DAB|/fdisjoint_sub->//]; apply/eqP/fsetP=> a. rewrite !inE; have [aC|] := boolP (a \in A `|` B); last first. by rewrite !inE => /norP [/negPf-> /negPf->]. by have /= := DAB [` fsubsetP ABsubC _ aC]; rewrite !inE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)