proposition: Lemma setU2_eq0P A B : (A \cup B = emptyset) <-> (A = emptyset /\ B = emptyset).
proof: Proof. split; [move => sube | by move => [-> ->]; rewrite setU2_id ]. split; apply /set0_P => t ta;case: (in_set0 (x:= t)); rewrite - sube; apply /setU2_P;fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)