proposition: Lemma mem_cross1 p : p \in cross1 = ((p.1 \in indexes) && (p.2 \in sref)).
proof: Proof. apply/allpairsP/idP=> [[[x1 y1]/= [Hx1 Hy1 ->]]|/andP[Hh Hw]]. by rewrite Hx1. by exists p; rewrite Hh Hw -surjective_pairing. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)