proposition: Lemma TS_upper_dim : forall A B C P Q, cut' A B P Q -> 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 HCut HD1 HD2 HD3 HD4 HD5 HD6 HD7 HD8 HD9 HD10. intros HCong1 HCong2 HCong3; destruct HCut as [_ HCut]; line P Q l HD1. assert (HC : cut l A B); [apply HCut; auto|clear HCut; rename HC into HCut]. 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|]. destruct HCut as [HNI1 [HNI2 [I [HI HBet]]]]. assert (HC' : ColH P Q I) by (exists l; auto). assert (HD11 : P <> I). { intro; subst; assert (HC : ColH A Q B) by (apply cong_preserves_col with A I B; Cong). apply HNC1; apply betH_expand in HBet; spliter; ColHR. } assert (HD12 : Q <> I). { intro; subst; assert (HC : ColH A P B) by (apply cong_preserves_col with A I B; auto with cong). apply HNC1; apply betH_expand in HBet; spliter; ColHR. } assert (HConga : CongaH I A P I A Q). { apply betH_expand in HBet; apply conga_out_conga with B P B Q; try apply outH_trivial; unfold outH; spliter; auto; apply th18_aux; Cong; intro; [apply HNC1|apply HNC2]; ColHR. } assert (HCong4 : CongH I P I Q). { apply betH_expand in HBet; spliter. destruct (th12 A I P A I Q) as [_ [_ ]]; Cong; try (intro; apply HNC1; ColHR). } assert (HC : ColH A B C). { elim (eq_dec_pointsH C I); intro HD13; subst; try solve[apply between_col in HBet; Col]. assert (HC : ColH A C I); [|apply betH_expand in HBet; spliter; ColHR]. apply betH_expand in HBet; 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