proposition: Lemma valid_pos2n p (s : seq nat) : valid_pos p -> size s = hw * hw -> pos2n p < size s.
proof: Proof. case: p => x y; rewrite /valid_pos /pos2n /= => /andP[Hx Hy]. nia. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)