proposition: Lemma TS_upper_dim_bis : forall A B C P Q I, BetH P I Q -> BetH I B A -> P <> Q -> A <> B -> A <> C -> B <> C -> A <> P -> A <> Q -> B <> P -> B <> Q -> C <> P -> C <> Q -> CongH A P A Q -> CongH B P B Q -> CongH C P C Q -> (Bet A B C \/ Bet B C A \/ Bet C A B).
proof: Proof. intros A B C P Q I HBet1 HBet2 HD1 HD2 HD3 HD4 HD5 HD6 HD7 HD8 HD9 HD10. intros HCong1 HCong2 HCong3. elim (colH_dec A P Q); intro HNC1; [elim (col_upper_dim A B C P Q); auto|]. elim (colH_dec B P Q); intro HNC2; [destruct (col_upper_dim B C A P Q) as [|[|]]; auto|]. assert (HConga : CongaH P B I Q B I). { apply th14 with A A; Bet; apply betH_expand in HBet1; apply betH_expand in HBet2; spliter; assert (HD11 : P <> I) by auto; assert (HD12 : Q <> I) by auto; [intro; apply HD11; apply inter_uniquenessH with P Q A B; try intro; Col| intro; apply HD12; apply inter_uniquenessH with P Q A B; try intro; Col|]. apply th18_aux; Cong; [intro; apply HD11; apply inter_uniquenessH with P Q A B; try intro; Col| intro; apply HD12; apply inter_uniquenessH with P Q A B; try intro; Col]. } assert (HCong4 : CongH I P I Q). { apply betH_expand in HBet1; apply betH_expand in HBet2; spliter. destruct (th12 B P I B Q I) as [_ [_ ]]; Cong; try (intro; apply HNC1; ColHR). } assert (HC : ColH A B C). { assert (HC1 : ColH A B I). { apply betH_expand in HBet1; apply betH_expand in HBet2; spliter. elim (col_upper_dim I A B P Q); Col. } elim (eq_dec_pointsH C I); intro HD11; subst; Col. assert (HC2 : ColH A C I); [|apply betH_expand in HBet2; spliter; ColHR]. apply betH_expand in HBet1; apply betH_expand in HBet2; spliter. elim (col_upper_dim I A C P Q); Col; intro HE; elim HE; clear HE; intro HE; apply bet_colH in HE; Col. } apply between_one in HC; Bet; unfold Bet. elim HC; clear HC; intro HC; [|elim HC; clear HC; intro HC]; auto. apply between_comm in HC; auto. Qed.
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