proposition: Theorem pos_test_trans: forall p1 p2 p3, pos_test p1 p2 = pos_test p2 p3 -> pos_test p1 p3 = pos_test p1 p2.
proof: Proof. intros p1 p2 p3; case p1; case p2; case p3; simpl; auto. intros x3 y3 x2 y2 x1 y1. case_eq (test x1 x2); intros H. case_eq (test x2 x3); intros H1. rewrite (test_trans x1 x2 x3); rewrite H; auto. assert (x2 = x3); subst. apply test_exact with (1 := H1); auto. rewrite H; auto. intros; discriminate. replace x1 with x2; auto. case_eq (test x2 x3); intros H1; auto. intros; apply test_trans; auto. apply sym_equal; apply test_exact with (1 := H); auto. case_eq (test x2 x3); intros H1. intros; discriminate. assert (x2 = x3); subst. apply test_exact with (1 := H1); auto. rewrite H; auto. rewrite (test_trans x1 x2 x3); rewrite H; auto. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia