proposition: Lemma valid_get_rect_rev i1 i2 j1 j2 : i1 < h -> i2 < w -> j1 < w -> j2 < h -> valid_pos (j1 * h + i1, j2 * w + i2).
proof: Proof. by move=> i1Lh i2Lw j1Lw j2Lh; rewrite /valid_pos /= hw_MhD // hw_MwD. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)