proposition: Lemma mem_cross p : p \in cross = ((p.1 < h) && (p.2 < w)).
proof: Proof. apply/allpairsP/idP=> [[[x1 y1]/= []]|/andP[Hh Hw]]. by rewrite !mem_iota !andTb !add0n => Hx Hy -> /=; apply/andP. by exists p; split; rewrite ?mem_iota // -surjective_pairing. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)