proposition: Lemma bet_cases : forall B C D1 D2, C<>B -> Definitions.BetS D1 B D2 -> Definitions.BetS D1 C D2 -> Definitions.BetS D1 B C \/ Definitions.BetS C B D2.
proof: Proof. intros. assert (T:Bet D1 C B \/ Bet D1 B C). apply (l5_3 D1 C B D2);unfold Definitions.BetS in *;spliter;Between. destruct T. right. unfold Definitions.BetS in *;spliter. assert (Bet C B D2) by (eBetween). unfold Definitions.BetS. repeat split;auto. left. unfold Definitions.BetS. unfold Definitions.BetS in *;spliter;repeat split;auto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Axioms.euclidean_axioms GeoCoq.Axioms.continuity_axioms GeoCoq.Meta_theory.Continuity.elementary_continuity_props GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates