proposition: Lemma col_cong_bet : forall A B C D, Col A B D -> Cong A B C D -> Bet A C B -> Bet C A D \/ Bet C B D.
proof: Proof. intros. prolong B A D1 B C. prolong A B D2 A C. assert(Cong A B C D1). eapply (l2_11 A C B C A D1). assumption. eapply between_exchange3. apply between_symmetry. apply H1. assumption. apply cong_pseudo_reflexivity. Cong. assert(D = D1 \/ Midpoint C D D1). eapply l7_20. apply bet_col in H1. apply bet_col in H2. induction (eq_dec_points A B). subst B. apply cong_symmetry in H0. apply cong_identity in H0. subst D. Col. eapply (col3 A B); Col. CongR. induction H7. subst D1. left. eapply between_exchange3. apply between_symmetry. apply H1. assumption. assert(Cong B A C D2). eapply (l2_11 B C A C B D2). Between. eapply between_exchange3. apply H1. assumption. apply cong_pseudo_reflexivity. Cong. assert(Midpoint C D2 D1). unfold Midpoint. split. induction(eq_dec_points A B). subst B. apply cong_symmetry in H0. apply cong_identity in H0. subst D. apply is_midpoint_id in H7. subst D1. Between. apply between_symmetry. induction(eq_dec_points B C). subst C. apply between_symmetry. apply cong_identity in H3. subst D1. Between. assert(Bet D1 C B). eBetween. assert(Bet C B D2). eBetween. eapply (outer_transitivity_between). apply H11. assumption. auto. unfold Midpoint in H7. spliter. eapply cong_transitivity. apply cong_symmetry. apply cong_commutativity. apply H8. eapply cong_transitivity. apply H0. Cong. assert(D = D2). eapply symmetric_point_uniqueness. apply l7_2. apply H7. apply l7_2. assumption. subst D2. right. eapply between_exchange3. apply H1. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch06_out_lines GeoCoq.Tarski_dev.Tactics.ColR