proposition: Lemma col_cong2_bet1 : forall A B C D, Col A B D -> Bet A C B -> Cong A B C D -> Cong A C B D -> Bet C B D.
proof: Proof. intros. induction(eq_dec_points A C). subst C. apply cong_symmetry in H2. apply cong_identity in H2. subst D. Between. assert(HH:=col_cong_bet A B C D H H1 H0). induction HH. assert(A = D /\ B = C). eapply bet_cong_eq. Between. eBetween. Cong. spliter. subst D. subst C. Between. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch06_out_lines GeoCoq.Tarski_dev.Tactics.ColR