proposition: Lemma midpoint_col : forall A B A' B' M, A <> B -> Midpoint M A A' -> Midpoint M B B' -> Col A B B' -> A' <> B' /\ Col A A' B' /\ Col B A' B'.
proof: Proof. intros. assert(A' <> B'). intro. apply H. assert(Cong A' B' A B). eapply l7_13. apply H0. assumption. apply cong_symmetry in H4. subst B'. apply cong_identity in H4. assumption. assert(HH0:= H0). assert(HH1:= H1). unfold Midpoint in HH0. unfold Midpoint in HH1. spliter. assert(Col M A A'). apply bet_col in H6. Col. assert(Col M B B'). apply bet_col in H4. Col. induction(eq_dec_points B B'). subst B'. apply l7_3 in H1. subst M. Col5. assert(Col A A' B'). assert(Col B M A). eapply col_transitivity_1. apply H10. Col. Col. assert(Col A M B'). eapply col_transitivity_1. apply H. Col. Col. induction(eq_dec_points A M). subst M. apply cong_symmetry in H7. apply cong_identity in H7. subst A'. Col. eapply col_transitivity_1. apply H13. Col. Col. repeat split; Col. induction(eq_dec_points A B'). subst B'. assert(A'=B). eapply l7_9; [|apply H1]. apply l7_2. assumption. subst A'. Col. ColR. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec