proposition: Lemma product_injective A B C D: nonempty (C \times D) -> A\times B = C\times D -> A = C /\ B = D.
proof: Proof. move => [x /setX_P [pa pb pc]] eq1. move: (setXp_i pb pc); rewrite - eq1 => /setXp_P [pd pe]. split; set_extens t => h. - by move:(setXp_i h pe); rewrite eq1; case /setXp_P. - by move:(setXp_i h pc); rewrite - eq1; case /setXp_P. - by move:(setXp_i pd h); rewrite eq1; case /setXp_P. - by move:(setXp_i pb h); rewrite - eq1; case /setXp_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)