proposition: Lemma bet_cong_eq : forall A B C D, Bet A B C -> Bet A C D -> Cong B C A D -> C = D /\ A = B.
proof: Proof. intros. assert(C = D). assert(Le A C A D) by (eapply l5_5_2; exists D; split; Cong). assert(Le C B C A) by (eapply l5_5_2; exists A; split; Between; Cong). assert(Cong A C A D) by (eapply le_anti_symmetry; try assumption; apply l5_6 with C B C A; Cong). apply between_cong with A; assumption. split; try assumption. subst D; apply sym_equal. eapply (between_cong C); Between; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch04_col