proposition: Lemma order_next_pos p1 p2 : p1 != p2 -> valid_pos p1 -> valid_pos p2 -> order_pos p1 p2 = order_pos (next p1) p2.
proof: Proof. case: p1 => x1 y1; case: p2 => x2 y2. rewrite xpair_eqE negb_and /valid_pos /next /= => p1Dp2 /andP[/= Hx1 Hy1] /andP[/= Hx2 Hy2]. repeat (case: eqP => //= ?); repeat (case: leqP => //= ?); lia. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)