proposition: Lemma l5_12_b : forall A B C, Col A B C -> Le A B A C -> Le B C A C -> Bet A B C.
proof: Proof. intros. unfold Col in H. induction H. assumption. induction H. assert(Le B C B A /\ Le C A B A). apply l5_12_a. assumption. spliter. assert(Cong A B A C). apply le_anti_symmetry. assumption. apply le_comm. assumption. assert(C = B). eapply between_cong. apply between_symmetry. apply H. apply cong_symmetry. assumption. subst B. apply between_trivial. assert(Le B A B C /\ Le A C B C). apply l5_12_a. apply between_symmetry. assumption. spliter. assert(Cong B C A C). apply le_anti_symmetry. assumption. assumption. assert(A = B). eapply between_cong. apply H. apply cong_symmetry. apply cong_commutativity. assumption. subst A. apply between_symmetry. apply between_trivial. Qed.
imports: GeoCoq.Tarski_dev.Ch04_col