proposition: Lemma bet_le_eq : forall A B C, Bet A B C -> Le A C B C -> A = B.
proof: Proof. intros. assert(Le C B C A). eapply l5_5_2. exists A. split. apply between_symmetry. assumption. apply cong_reflexivity. assert(Cong A C B C). apply le_anti_symmetry. assumption. apply le_comm. assumption. apply sym_equal. eapply between_cong. apply between_symmetry. apply H. apply cong_commutativity. apply cong_symmetry. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch04_col