proposition: Lemma get_rect x y g : size g = hw * hw -> x < hw -> y < hw -> get (x, y) g = nth out (rect (x %/ h * h + y %/ w) g) (x %% h * w + y %% w).
proof: Proof. move=> Hs xLhw yLhw. have hw_pos : 0 < hw by apply: leq_ltn_trans xLhw. have h_pos := h_pos xLhw; have w_pos := w_pos xLhw. have x_d_h := hw_divh xLhw; have x_m_h := hw_modh xLhw. have y_d_w := hw_divw yLhw; have y_m_w := hw_modw yLhw. rewrite nth_take_and_drop. - rewrite nth_drop /get /pos2n /= !divnMDl // !modnMDl. rewrite modn_small // [(y %/ w)%/ h]divn_small // addn0. rewrite [(_ %% _)%/ _]divn_small // addn0. rewrite modn_mod [x in LHS](divn_eq _ h) [y in LHS](divn_eq _ w). congr nth; lia. - by rewrite w_pos -[w]mul1n leq_mul2r eqn0Ngt w_pos. - by rewrite hw_modwMDmod. rewrite modnMDl divnMDl // modn_small // [(_ %/ _) %/ h]divn_small //. rewrite addn0 size_drop Hs. rewrite /hw in hw_pos xLhw yLhw *; nia. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)