proposition: Lemma upper_dim : forall A B C P Q , P <> Q -> Cong A P A Q -> Cong B P B Q -> Cong C P C Q -> (Bet A B C \/ Bet B C A \/ Bet C A B).
proof: Proof. intros. destruct P; destruct Q; try solve [intuition]; try (apply cong_aux in H0; apply cong_aux in H1; apply cong_aux in H2); try (apply cong_aux_2 in H0; apply cong_aux_2 in H1; apply cong_aux_2 in H2); try (apply cong_aux_3 in H0; apply cong_aux_3 in H1; apply cong_aux_3 in H2); try (apply cong_aux_4 in H0; apply cong_aux_4 in H1; apply cong_aux_4 in H2); try (apply cong_aux_5 in H0; apply cong_aux_5 in H1; apply cong_aux_5 in H2); try (apply cong_aux_6 in H0; apply cong_aux_6 in H1; apply cong_aux_6 in H2); try (apply cong_sym in H0; apply cong_sym in H1; apply cong_sym in H2); try (apply cong_aux in H0; apply cong_aux in H1; apply cong_aux in H2); try (apply cong_aux_2 in H0; apply cong_aux_2 in H1; apply cong_aux_2 in H2); try (apply cong_aux_3 in H0; apply cong_aux_3 in H1; apply cong_aux_3 in H2); try (apply cong_aux_4 in H0; apply cong_aux_4 in H1; apply cong_aux_4 in H2); try (apply cong_aux_5 in H0; apply cong_aux_5 in H1; apply cong_aux_5 in H2); try (apply cong_aux_6 in H0; apply cong_aux_6 in H1; apply cong_aux_6 in H2); intuition; subst; unfold Bet; tauto. Qed.
imports: GeoCoq.Axioms.tarski_axioms