proposition: Lemma tuto_setCU : forall A B, ~: (A :|: B) = ~: A :&: ~: B.
proof: Proof. by move=> A B; apply/setP => x; rewrite !inE -negb_or. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finset)