proposition: Lemma le_cases : forall A B C D, Le A B C D \/ Le C D A B.
proof: Proof. intros. induction(eq_dec_points A B). subst B; left; apply le_trivial. assert (exists X : Tpoint, (Bet A B X \/ Bet A X B) /\ Cong A X C D) by (eapply (segment_construction_2 B A C D);auto). ex_and H0 X. induction H0. left; apply l5_5_2; exists X; split; assumption. right; unfold Le; exists X; split; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch04_col