proposition: Lemma size_column j g : j < hw -> size g = hw * hw -> size (column j g) = hw.
proof: Proof. move=> jLhw Hs. rewrite size_take_and_drop ?muln1 // size_drop {}Hs. rewrite addn1; nia. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)