proposition: Lemma valid_pos_eq p1 p2 : valid_pos p1 -> valid_pos p2 -> pos2n p1 = pos2n p2 -> p1 = p2.
proof: Proof. case: p1 => x1 y1; case: p2 => x2 y2. rewrite /valid_pos /pos2n /= =>/andP[x1L y1L] /andP[x2L y2L] HH; congr (_ , _). apply: etrans (_ : (x1 * hw + y1) %/ hw = _). by rewrite divnMDl ?divn_small; lia. by rewrite HH divnMDl ?divn_small; lia. apply: etrans (_ : (x1 * hw + y1) %% hw = _). by rewrite modnMDl ?modn_small; lia. by rewrite HH modnMDl ?modn_small; lia. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)