proposition: Lemma mem_cross2 p : (p \in cross2) = valid_pos p.
proof: Proof. case: p => x1 y1; rewrite /valid_pos /=. apply/allpairsP/idP => [[[x2 y2] /=]|/andP[x1Lw y1Lw]]. by rewrite !mem_iota /= add0n => [] [xLhw yLhw [-> ->]]; rewrite xLhw. by exists (x1, y1); rewrite !mem_iota; split. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)