proposition: Lemma get_rect_rev i j g : size g = hw * hw -> i < hw -> j < hw -> get (j %/ h * h + i %/ w, j %% h * w + i %% w) g = nth out (rect j g) i.
proof: Proof. move=> Hs iLhw jLhw. have hw_pos : 0 < hw by apply: leq_ltn_trans iLhw. have h_pos := h_pos iLhw; have w_pos := w_pos iLhw. have j_d_h := hw_divh jLhw; have i_m_h := hw_modh jLhw. have i_d_w := hw_divw iLhw; have i_m_w := hw_modw iLhw. rewrite get_rect ?hw_MwD ?hw_MhD //. rewrite !divnMDl // !modnMDl; congr (nth _ (rect _ _) _). by rewrite (divn_small i_d_w) (divn_small i_m_w) !addn0 -divn_eq. by rewrite modn_mod (modn_small i_d_w) -divn_eq. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)