proposition: Lemma setX_0 A B: A \times B = emptyset -> (A = emptyset \/ B = emptyset).
proof: Proof. move=> pe; case: (emptyset_dichot A);first by left. by case => t tx; right; apply /set0_P => u up; empty_tac1 (J t u). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)