proposition: Lemma l5_5_1 : forall A B C D, Le A B C D -> exists x, Bet A B x /\ Cong A x C D.
proof: Proof. unfold Le. intros. ex_and H P. prolong A B x P D. exists x. split. assumption. eapply l2_11;eauto. Qed.
imports: GeoCoq.Tarski_dev.Ch04_col