proposition: Lemma tuto_disjointU : forall A B C, [disjoint predU A B & C] = [disjoint A & C] && [disjoint B & C].
proof: Proof. move=> A B C. case dAC: ([disjoint A & C])=> /=. rewrite /disjoint /pred0b; congr (_ == 0); apply: eq_card=> x. rewrite -[x \in [predI _ & _]]/(((x \in A) || (x \in B)) && (x \in C)) andb_orl. suff -> : (x \in A) && (x \in C) = false by done. by move/pred0P: dAC; move/(_ x). apply/pred0P=> nABC; case/pred0Pn: dAC=> x; case/andP=> /= Ax Cx. move: (nABC x)=> /=. by rewrite Cx /= -[x \in [predU A & B]]/((x \in A) || (x \in B)) Ax. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finset)