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