proposition: Lemma disjointness1 M N: exists r, let M1 := zprod2 M (singleton r) in [/\ ~ (inc r M) , disjoint M M1 & disjoint N M1].
proof: Proof. move: (disjointness (M \cup (union (M \cup N)))) => [K [pa pb]]. have : (~ (inc K (union (M \cup N)))) by dneg k; fprops. have kM: (~ inc K M) by dneg km; fprops. have d1: (disjoint (union2 M N) (zprod2 M (singleton K))). apply: disjoint_pr => u uu us. move: (zprod_singleton kM) => [pc pd]; move: (pd _ us) => [v vM ud]. case: pb; apply: setU2_2; apply /setU_P; exists u => //; rewrite ud; fprops. move=> nku;exists K;split => //;apply: disjoint_pr => u um aux; empty_tac1 u. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)