proposition: Lemma euclidT : forall A B C D T, Bet A D T -> Bet B D C -> A <> D -> exists X, exists Y, Bet A B X /\ Bet A C Y /\ Bet X T Y.
proof: Proof. assert (H := GI_to_T_PED). intros A B C D T HBet1 HBet2 HDiff1. elim (eq_dec_points B D); intro HDiff2; [treat_equalities; exists T, C; Between|]. elim (eq_dec_points D C); intro HDiff3; [treat_equalities; exists B, T; Between|]. elim (col_dec A B C); intro HCol; [|apply euclidG with D; auto]. clear HDiff2; clear HDiff3. do 2 (try (elim HCol; clear HCol; intro HCol)); rename HCol into HBet3. { elim (eq_dec_points A B); intro HDiff2; [treat_equalities; exists T; exists C; Between|]. elim (l5_2 A B C T); eBetween; intro HBet4. { elim (eq_dec_points B C); intro HDiff3; [treat_equalities; exists T; exists T; Between|]. exists B; exists T; do 2 (split; Between); eBetween. } { elim (eq_dec_points B T); intro HDiff3; [treat_equalities; exists B; exists C; Between|]. exists B; exists C; Between. } } { elim (eq_dec_points A C); intro HDiff2; [treat_equalities; exists B; exists T; Between|]. elim (l5_2 A C B T); eBetween; intro HBet4. { elim (eq_dec_points B C); intro HDiff3; [treat_equalities; exists T; exists T; Between|]. exists T; exists C; repeat (split; Between); eBetween. } { exists B; exists C; Between. } } { elim (l5_3 B A D C); Between; intro HBet4. { elim (eq_dec_points A B); intro HDiff2; [treat_equalities; exists T; exists C; Between|]. elim (l5_2 B A C T); eBetween; intro HBet5. { exists B; exists T; Between. } { exists B; exists C; do 2 (split; Between). apply outer_transitivity_between2 with A; eBetween. intro; treat_equalities; intuition. } } { elim (l5_2 A D B T); Between; intro HBet5. { elim (eq_dec_points B D); intro HDiff2; [treat_equalities; exists T; exists C; Between|]. exists T; exists C; do 2 (try split; Between); eBetween. } { exists B; exists C; do 2 (split; Between). apply outer_transitivity_between with A; eBetween; try (intro; treat_equalities; intuition). } } } Qed.
imports: GeoCoq.Axioms.tarski_axioms GeoCoq.Axioms.gupta_inspired_variant_axioms GeoCoq.Tarski_dev.Ch05_bet_le