proposition: Lemma l5_5_2 : forall A B C D, (exists x, Bet A B x /\ Cong A x C D) -> Le A B C D.
proof: Proof. intros. ex_and H P. unfold Le. assert (exists B' : Tpoint, Bet C B' D /\ Cong_3 A B P C B' D) by (eapply l4_5;auto). ex_and H1 y. exists y. unfold Cong_3 in *;intuition. Qed.
imports: GeoCoq.Tarski_dev.Ch04_col