proposition: Theorem lit_test_trans: forall l1 l2 l3, lit_test l1 l2 = lit_test l2 l3 -> lit_test l1 l3 = lit_test l1 l2.
proof: Proof. Proof with auto. intros l1 l2 l3; case l1; case l2; case l3; simpl... intros p3 z3 p2 z2 p1 z1. case_eq (pos_test p1 p2); intros H. case_eq (pos_test p2 p3); intros H1. rewrite (pos_test_trans p1 p2 p3); rewrite H... assert (p2 = p3); subst. apply pos_test_exact with (1 := H1)... rewrite H... intros; discriminate. replace p1 with p2... case_eq (pos_test p2 p3); intros H1... intros; apply test_trans... apply sym_equal; apply pos_test_exact with (1 := H)... case_eq (pos_test p2 p3); intros H1. intros; discriminate. assert (p2 = p3); subst. apply pos_test_exact with (1 := H1)... rewrite H... rewrite (pos_test_trans p1 p2 p3); rewrite H... Qed.
imports: List UList Permutation Div OrderedList ListOp Lia