proposition: Theorem pos_test_anti_sym: forall p1 p2, pos_test p1 p2 = opp (pos_test p2 p1).
proof: Proof. intros p1 p2; case p1; case p2; simpl; auto. intros x2 y2 x1 y1; rewrite (test_anti_sym x1 x2). case (test x2 x1); simpl; auto. apply test_anti_sym. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia