proposition: Lemma col_upper_dim : forall A B C P Q, ColH A 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 HBet HD1 HD2 HD3 HD4 HD5 HD6 HD7 HD8 HD9 HD10. intros HCong1 HCong2 HCong3; apply congH_colH_betH in HBet; auto. assert (HNC1 : ~ ColH B P Q). { intro H; apply congH_colH_betH in H; auto. elim (betH2_out P A B Q); auto; intro HBet'. { assert (BetH Q B A) by (destruct (betH_trans0 P A B Q); Bet). apply betH_congH2__False with P A B Q A B; Cong. } { assert (BetH Q A B) by (destruct (betH_trans0 P B A Q); Bet). apply betH_congH2__False with P B A Q B A; Cong. } } assert (HNC2 : ~ ColH C P Q). { intro H; apply congH_colH_betH in H; auto. elim (betH2_out P A C Q); auto; intro HBet'. { assert (BetH Q C A) by (destruct (betH_trans0 P A C Q); Bet). apply betH_congH2__False with P A C Q A C; Cong. } { assert (BetH Q A C) by (destruct (betH_trans0 P C A Q); Bet). apply betH_congH2__False with P C A Q C A; Cong. } } elim (plane_separation_2D _ _ _ _ HNC1 HNC2); intro HS. { destruct HS as [_ HCut]; line P Q l HD1. assert (HC : cut l B C); [apply HCut; auto|clear HCut; rename HC into HCut]. destruct HCut as [HNI1 [HNI2 [I [HI HBet']]]]. assert (HD11 : P <> I). { intro; subst; assert (HC : ColH B Q C) by (apply cong_preserves_col with B I C; Cong). apply HNC1; apply betH_expand in HBet'; spliter; ColHR. } assert (HD12 : Q <> I). { intro; subst; assert (HC : ColH B P C) by (apply cong_preserves_col with B I C; auto with cong). apply HNC1; apply betH_expand in HBet'; spliter; ColHR. } assert (HC' : ColH P Q I) by (exists l; auto). assert (HConga : CongaH I B P I B Q). { apply betH_expand in HBet'; apply conga_out_conga with C P C 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 B I P B I Q) as [_ [_ ]]; Cong; try (intro; apply HNC1; ColHR). } elim (eq_dec_pointsH A I); intro HD13; [subst; right; right; unfold Bet; Bet|]. assert (HBet'' : ColH I P Q); Col; clear HC'. apply congH_colH_betH in HBet''; auto. elim (betH2_out P A I Q); auto; intro HF; exfalso. { assert (BetH Q I A) by (destruct (betH_trans0 P A I Q); Bet). apply betH_congH2__False with P A I Q A I; Cong. } { assert (BetH Q A I) by (destruct (betH_trans0 P I A Q); Bet). apply betH_congH2__False with P I A Q I A; Cong. } } { assert (HNC3 : ~ ColH P B C). { intro HC1; assert (H : ColH C P B) by Col; assert (HC2 : ColH B C Q) by (apply cong_preserves_col_stronger with B C P; Cong; Col). assert (HBet1 : BetH P B Q) by (apply congH_colH_betH; auto; ColHR). assert (HBet2 : BetH P C Q) by (apply congH_colH_betH; auto; ColHR). clear HC1; apply between_one in H; auto; elim H; clear H; intro HBet3; [apply between_only_one' in HBet2; destruct HBet2 as [_ HF]; apply HF; eauto with bet|elim HBet3; clear HBet3; intro HBet3]. { assert (HBet4 : BetH Q C B) by (destruct (betH_trans0 P B C Q); Bet). apply betH_congH2__False with P B C Q B C; Cong. } { assert (HBet4 : BetH Q B C) by (destruct (betH_trans0 P C B Q); Bet). apply betH_congH2__False with P C B Q C B; Cong. } } assert (HNC4 : ~ ColH Q B C). { intro HC1; assert (HC2 : ColH B C P); [|apply HNC3; Col]; apply cong_preserves_col_stronger with B C Q; Cong; Col. } elim (plane_separation_2D _ _ _ _ HNC3 HNC4); intro HS'. { destruct HS' as [_ HS']; line B C lBC HD4; elim (HS' lBC); auto. intros _ [_ [I [HI HBet']]]. assert (HBet2 : ColH B I C) by (exists lBC; auto). apply between_one in HBet2; try solve[intro; subst; apply betH_expand in HBet'; spliter; Col]. elim HBet2; clear HBet2; intro HBet''. { line P Q lPQ HD1; destruct HS as [_ HS]; assert (HS4 : same_side B C lPQ) by (apply HS; auto); apply same_side_not_cut in HS4; exfalso; apply HS4. split; [intro; apply HNC1; exists lPQ; auto|]. split; [intro; apply HNC2; exists lPQ; auto|]. exists I; split; auto; apply betH_line in HBet'. destruct HBet' as [l [HI2 [HI3 HI4] ]]; apply morph with l; auto. apply line_uniqueness with P Q; auto. } { elim HBet''; clear HBet''; intro HBet''. { assert (HConga : CongaH P C I Q C I). { apply th14 with B B; Bet; apply betH_expand in HBet'; apply betH_expand in HBet''; spliter; assert (HD11 : P <> I) by auto; assert (HD12 : Q <> I) by auto; [intro; apply HD11; apply inter_uniquenessH with P Q C B; try intro; Col| intro; apply HD12; apply inter_uniquenessH with P Q C B; try intro; Col|]. apply th18_aux; Cong; [intro; apply HD11; apply inter_uniquenessH with P Q C B; try intro; Col| intro; apply HD12; apply inter_uniquenessH with P Q C B; try intro; Col]. } assert (HCong4 : CongH I P I Q). { apply betH_expand in HBet'; apply betH_expand in HBet''; spliter. destruct (th12 C P I C Q I) as [_ [_ ]]; Cong; try (intro; apply HNC1; ColHR). } elim (eq_dec_pointsH A I); intro HD13; [subst; right; left; unfold Bet; Bet|]. assert (HBet''' : ColH I P Q) by (apply betH_expand in HBet'; spliter; Col). apply congH_colH_betH in HBet'''; try solve[apply betH_expand in HBet'; spliter; Col]. elim (betH2_out P A I Q); auto; intro HF; exfalso. { apply betH_expand in HBet'; spliter. assert (BetH Q I A) by (destruct (betH_trans0 P A I Q); Bet). apply betH_congH2__False with P A I Q A I; Cong. } { apply betH_expand in HBet'; spliter. assert (BetH Q A I) by (destruct (betH_trans0 P I A Q); Bet). apply betH_congH2__False with P I A Q I A; Cong. } } { assert (HConga : CongaH P B I Q B I). { apply th14 with C C; Bet; apply betH_expand in HBet'; apply betH_expand in HBet''; spliter; assert (HD11 : P <> I) by auto; assert (HD12 : Q <> I) by auto; [intro; apply HD11; apply inter_uniquenessH with P Q B C; try intro; Col| intro; apply HD12; apply inter_uniquenessH with P Q B C; try intro; Col|]. apply th18_aux; Cong; [intro; apply HD11; apply inter_uniquenessH with P Q B C; try intro; Col| intro; apply HD12; apply inter_uniquenessH with P Q B C; try intro; Col]. } assert (HCong4 : CongH I P I Q). { apply betH_expand in HBet'; apply betH_expand in HBet''; spliter. destruct (th12 B P I B Q I) as [_ [_ ]]; Cong; try (intro; apply HNC1; ColHR). } elim (eq_dec_pointsH A I); intro HD13; [subst; left; unfold Bet; Bet|]. assert (HBet''' : ColH I P Q) by (apply betH_expand in HBet'; spliter; Col). apply congH_colH_betH in HBet'''; try solve[apply betH_expand in HBet'; spliter; Col]. elim (betH2_out P A I Q); auto; intro HF; exfalso. { apply betH_expand in HBet'; spliter. assert (BetH Q I A) by (destruct (betH_trans0 P A I Q); Bet). apply betH_congH2__False with P A I Q A I; Cong. } { apply betH_expand in HBet'; spliter. assert (BetH Q A I) by (destruct (betH_trans0 P I A Q); Bet). apply betH_congH2__False with P I A Q I A; Cong. } } } } { assert (H : outH B P Q); [|apply outH_expand in H; spliter; exfalso; apply HNC1; Col]. apply cong_4_uniqueness with C B P P C; try apply conga_refl; try apply same_side_prime_refl; try (intro; apply HNC3; Col); auto. apply th18_aux; Cong; intro; [apply HNC3|apply HNC4]; Col. } } 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