proposition: Lemma upper_dim : forall A B C P Q, P <> Q -> A <> B -> A <> C -> B <> C -> 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. unfold Cong; intros A B C P Q HD1 HD2 HD3 HD4 HCong1 HCong2 HCong3. elim HCong1; clear HCong1; intro HCong1; [|spliter; repeat subst; intuition]. elim HCong2; clear HCong2; intro HCong2; [|spliter; repeat subst; intuition]. elim HCong3; clear HCong3; intro HCong3; [|spliter; repeat subst; intuition]. destruct HCong1 as [HCong1 [HD5 HD6]]. destruct HCong2 as [HCong2 [HD7 HD8]]. destruct HCong3 as [HCong3 [HD9 HD10]]. 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|]. elim (colH_dec C P Q); intro HNC3; [destruct (col_upper_dim C A B P Q) as [|[|]]; auto|]. elim (plane_separation_2D _ _ _ _ HNC1 HNC2); intro HS1; [elim (TS_upper_dim A B C P Q); auto|]. elim (plane_separation_2D _ _ _ _ HNC1 HNC3); intro HS2; [destruct (TS_upper_dim C A B P Q) as [|[|]]; try apply cut'_comm; auto|]. assert (HNC4 : ~ ColH P A B). { intro HC1; assert (H : ColH B P A) by Col; assert (HC2 : ColH A B Q) by (apply cong_preserves_col_stronger with A B P; Cong; Col). assert (HBet1 : BetH P A Q) by (apply congH_colH_betH; auto; ColHR). assert (HBet2 : BetH P B 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 B A) by (destruct (betH_trans0 P A B Q); Bet). apply betH_congH2__False with P A B Q A B; Cong. } { assert (HBet4 : 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 (HNC5 : ~ ColH Q A B). { intro HC1; assert (HC2 : ColH A B P); [|apply HNC4; Col]; apply cong_preserves_col_stronger with A B Q; Cong; Col. } elim (plane_separation_2D _ _ _ _ HNC4 HNC5); intro HS3. { destruct HS3 as [_ HS3]; line A B lAB HD2; elim (HS3 lAB); auto. intros _ [_ [I [HI HBet1]]]; assert (HBet2 : ColH A I B) by (exists lAB; auto). apply between_one in HBet2; try (elim HBet2; clear HBet2; intro HBet2); try (intro; intro; subst; apply betH_expand in HBet1; spliter; Col). { line P Q lPQ HD1; destruct HS1 as [_ HS1]; assert (HS4 : same_side A B lPQ) by (apply HS1; 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 HBet1; destruct HBet1 as [l [HI2 [HI3 HI4] ]]; apply morph with l; auto. apply line_uniqueness with P Q; auto. } { elim HBet2; clear HBet2; intro HBet2; [elim (TS_upper_dim_bis A B C P Q I)|elim (TS_upper_dim_bis B A C P Q I)]; auto; intro HE; [|elim HE; clear HE; intro HE]; apply bet_comm in HE; auto. } } { assert (H : outH A P Q); [|apply outH_expand in H; spliter; exfalso; apply HNC1; Col]. apply cong_4_uniqueness with B A P P B; try apply conga_refl; try apply same_side_prime_refl; try (intro; apply HNC4; Col); auto. apply th18_aux; Cong; intro; [apply HNC4|apply HNC5]; 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