proposition: Theorem valid_pos_eq: forall p1 p2, valid_pos p1 -> valid_pos p2 -> pos2n p1 = pos2n p2 -> p1 = p2.
proof: Proof. intros (x1, y1) (x2, y2); simpl; intros (H1, H2) (H3, H4) H5. assert (x1 = x2); try f_equal; auto; try subst x2. apply lexico_mult with (3 := H5); auto. apply Nat.add_cancel_l with (1 := H5). Qed.
imports: List UList Permutation Div OrderedList ListOp Lia