proposition: Lemma upper_dimT : forall A B C P Q, P <> Q -> CongG A P A Q -> CongG B P B Q -> CongG C P C Q -> (BetG A B C \/ BetG B C A \/ BetG C A B).
proof: Proof. intros A B C P Q HPQ HCong1 HCong2 HCong3. elim (point_equality_decidabilityG A B); intro HAB; try (rewrite HAB in *; clear HAB); elim (point_equality_decidabilityG A C); intro HAC; try (rewrite HAC in *; clear HAC); elim (point_equality_decidabilityG B C); intro HBC; try (rewrite HBC in *; clear HBC). { left; apply between_trivialT. } { right; right; apply between_trivialT. } { left; apply between_trivialT. } { right; right; apply between_trivialT. } { left; apply between_trivialT. } { right; left; apply between_trivialT. } { left; apply between_trivialT. } { apply upper_dimG with P Q; auto. } Qed.
imports: GeoCoq.Axioms.tarski_axioms GeoCoq.Axioms.gupta_inspired_variant_axioms GeoCoq.Tarski_dev.Ch05_bet_le