proposition: Lemma fdisjoint_sub {A B} : [disjoint A & B]%fset -> forall C : {fset K}, [disjoint fsub C A & fsub C B]%bool.
proof: Proof. move=> disjointAB C; apply/pred0P => a /=; rewrite !inE. by have /eqP /fsetP /(_ (val a)) := disjointAB; rewrite !inE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)