proposition: Lemma order_next_anti p1 p2 : p1 != p2 -> order_pos p1 p2 = ~~ (order_pos p2 p1).
proof: Proof. case: p1 => x1 y1; case: p2 => x2 y2 /=. by rewrite xpair_eqE negb_and; do 2 case: ltngtP. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)