proposition: Lemma tarski_upper_dim : forall A B C P Q R, P <> Q -> Q <> R -> P <> R -> Cong A P A Q -> Cong B P B Q -> Cong C P C Q -> Cong A P A R -> Cong B P B R -> Cong C P C R -> (Bet A B C \/ Bet B C A \/ Bet C A B).
proof: Proof. cut upper_dim_3_axiom. unfold upper_dim_3_axiom; auto. cut plane_intersection_axiom. apply upper_dim_3_equivalent_axioms; simpl; tauto. intros A B C D E F P HP1 HP2. apply coplanar_plane in HP1. apply coplanar_plane in HP2. destruct HP1 as [p]. destruct HP2 as [q]. spliter. destruct (plane_intersection P p q) as [Q]; [assumption..|]. spliter. exists Q. repeat split; [..|assumption]. apply plane_coplanar with p; assumption. apply plane_coplanar with q; assumption. Defined.
imports: Setoid Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop GeoCoq.Axioms.gupta_inspired_variant_axioms GeoCoq.Meta_theory.Models.gupta_inspired_to_tarski GeoCoq.Tactics.Coinc.tactics_axioms GeoCoq.Tactics.Coinc.ColR GeoCoq.Meta_theory.Dimension_axioms.upper_dim_3 GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates GeoCoq.Axioms.hilbert_axioms