proposition: Theorem lit_test_anti_sym: forall l1 l2, lit_test l1 l2 = opp (lit_test l2 l1).
proof: Proof. intros l1 l2; case l1; case l2; simpl; auto. intros p2 z2 p1 z1; rewrite (pos_test_anti_sym p1 p2). case (pos_test p2 p1); simpl; auto. apply test_anti_sym. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia