proposition: Lemma valid_pos_next p : valid_pos p -> pos2n (next p) < hw * hw -> valid_pos (next p).
proof: Proof. case: p => x y; rewrite /next /pos2n /valid_pos /= => /andP[Hx Hy]. case: eqP => Hw /=; nia. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)