proposition: Lemma size_rect i g : i < hw -> size g = hw * hw -> size (rect i g) = hw.
proof: Proof. rewrite /hw => iLhw Hs. have h_pos := h_pos iLhw; have w_pos := w_pos iLhw. have i_d_h := hw_divh iLhw; have i_m_h := hw_modh iLhw. by rewrite size_take_and_drop // size_drop Hs /hw; nia. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)