proposition: Theorem pos_test_exact: forall p1 p2, pos_test p1 p2 = eq -> p1 = p2.
proof: Proof. intros p1 p2; case p1; case p2; simpl; auto. intros x2 y2 x1 y1; case_eq (test x1 x2); intros H; auto. intros; discriminate. intros H1; f_equal; apply test_exact; auto. intros; discriminate. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia