proposition: Lemma between_one : forall A B C, A <> B -> A <> C -> B <> C -> ColH A B C -> BetH A B C \/ BetH B C A \/ BetH B A C.
proof: Proof. intros A B C HD1 HD2 HD3 HC. destruct (ncolH_exists _ _ HD2) as [D HNC1]. assert (HD4 : B <> D) by (intro; subst; apply HNC1; Col). destruct (between_out _ _ HD4) as [G HBet1]. assert (HD5 : A <> D) by (intro; subst; Col); line A D lAD HD5. assert (HD6 : C <> D) by (intro; subst; Col); line C D lCD HD6. assert (HNC2 : ~ ColH B G C) by (intro; apply betH_expand in HBet1; spliter; apply HNC1; ColHR). assert (HNC3 : ~ ColH B G A) by (intro; apply betH_expand in HBet1; spliter; apply HNC1; ColHR). assert (HNI1 : ~ IncidL C lAD) by (intro; apply HNC1; exists lAD; auto). assert (HNI2 : ~ IncidL A lCD) by (intro; apply HNC1; exists lCD; auto). assert (HCut1 : cut lAD B G). { apply betH_expand in HBet1; spliter. split; [intro; assert (ColH A B D) by (exists lAD; auto); apply HNC1; ColHR|]. split; [intro; assert (ColH A D G) by (exists lAD; auto); apply HNC1; ColHR|]. exists D; auto. } assert (HCut2 : cut lCD B G). { apply betH_expand in HBet1; spliter. split; [intro; assert (ColH B C D) by (exists lCD; auto); apply HNC1; ColHR|]. split; [intro; assert (ColH C D G) by (exists lCD; auto); apply HNC1; ColHR|]. exists D; auto. } destruct (plane_existence B G C HNC2) as [bgc]. spliter. destruct (plane_existence B G A HNC3) as [bga]. spliter. assert (HLP1 : IncidLP lAD bgc). { apply (line_on_plane A D); trivial. apply (line_on_plane' B C); Col. apply betH_colH in HBet1; spliter. apply (line_on_plane' B G); Col. } assert (HLP2 : IncidLP lCD bga). { apply (line_on_plane C D); trivial. apply (line_on_plane' A B); Col. apply betH_colH in HBet1; spliter. apply (line_on_plane' B G); Col. } elim (pasch B G C lAD bgc); trivial; clear dependent bgc; intro HCut3; elim (pasch B G A lCD bga); trivial; clear dependent bga; intro HCut4. { destruct HCut3 as [_ [_ [I [HI3 HBet2]]]]. elim (eq_dec_pointsH A I); intro HD7; [subst; right; right; auto|]. assert (I = A); [|subst; right; right; auto]. apply betH_expand in HBet2; spliter. assert (ColH A D I) by (exists lAD; auto). apply inter_uniquenessH with B C D A; try (intro; apply HNC1); Col; ColHR. } { destruct HCut3 as [_ [_ [I [HI3 HBet2]]]]. elim (eq_dec_pointsH A I); intro HD7; [subst; right; right; auto|]. assert (I = A); [|subst; right; right; auto]. apply betH_expand in HBet2; spliter. assert (ColH A D I) by (exists lAD; auto). apply inter_uniquenessH with B C D A; try (intro; apply HNC1); Col; ColHR. } { destruct HCut4 as [_ [_ [I [HI3 HBet2]]]]. elim (eq_dec_pointsH C I); intro HD7; [subst; right; left; auto|]. assert (I = C); [|subst; right; left; auto]. apply betH_expand in HBet2; spliter. assert (ColH C D I) by (exists lCD; auto). apply inter_uniquenessH with A B D C; try (intro; apply HNC1); Col; ColHR. } { destruct HCut3 as [_ [_ [E [HI3 HBet2]]]]. destruct HCut4 as [_ [_ [F [HI4 HBet3]]]]. assert (HNC4 : ~ ColH A G E). { intro; apply betH_expand in HBet1; apply betH_expand in HBet2; spliter. apply HNC1; ColHR. } assert (HD7 : C <> F); [|line C F lCF HD7]. { apply betH_expand in HBet2; apply betH_expand in HBet3; spliter. intro; subst; apply HNC4; ColHR. } assert (HNI3 : ~ IncidL E lCF). { apply betH_expand in HBet1; apply betH_expand in HBet2; apply betH_expand in HBet3; spliter. intro; assert (ColH C E F) by (exists lCF; auto); apply HNC1; ColHR. } assert (HCut3 : cut lCF A G). { apply betH_expand in HBet1; apply betH_expand in HBet2; apply betH_expand in HBet3; spliter. split; [intro; assert (ColH A C F) by (exists lCF; auto); apply HNC1; ColHR|]. split; [intro; assert (ColH C F G) by (exists lCF; auto); apply HNC1; ColHR|]. exists F; auto; split; try apply between_comm; auto. } destruct (plane_existence A G E HNC4) as [p]. spliter. assert (HLP : IncidLP lCF p). { apply (line_on_plane C F); trivial. apply betH_colH in HBet2; spliter. apply (line_on_plane' G E); Col. apply betH_colH in HBet3; spliter. apply (line_on_plane' G A); Col. } elim (pasch A G E lCF p); trivial; clear dependent p; intro HCut4. { destruct HCut4 as [_ [_ [I [HI5 HBet4]]]]. assert (I = D); [|subst]. { apply betH_expand in HBet4; spliter. apply inter_uniquenessH with C D A E; try intro; subst; Col; [|exists lAD]; auto. assert (ColH C D F) by (exists lCD; auto). assert (ColH C F I) by (exists lCF; auto); ColHR. } assert (HNC5 : ~ ColH A E C) by (intro; apply betH_expand in HBet4; spliter; apply HNC1; ColHR). assert (HD8 : B <> D) by (intro; subst; apply HNC1; Col). line B D lBD HD8; assert (HNI4 : ~ IncidL C lBD) by (intro; assert (ColH B C D) by (exists lBD; auto); apply HNC1; ColHR). assert (HCut4 : cut lBD A E). { apply betH_expand in HBet4; spliter. split; [intro; assert (ColH A B D) by (exists lBD; auto); apply HNC1; ColHR|]. split; [intro; assert (ColH B D E) by (exists lBD; auto); apply HNC1; ColHR|]. exists D; auto. } destruct (plane_existence A E C HNC5) as [p]. spliter. assert (HLP : IncidLP lBD p). { apply (line_on_plane B D); trivial. apply (line_on_plane' A C); Col. apply betH_colH in HBet4; spliter. apply (line_on_plane' A E); Col. } elim (pasch A E C lBD p); trivial; clear dependent p; intro HCut5. { destruct HCut5 as [_ [_ [I [HI6 HBet5]]]]. assert (I = B); [|subst; left; auto]. apply betH_expand in HBet5; spliter. apply inter_uniquenessH with A C D B; Col; exists lBD; auto. } { destruct HCut5 as [_ [_ [I [HI6 HBet5]]]]. assert (I = G); [|subst]. { apply betH_expand in HBet1; apply betH_expand in HBet2; apply betH_expand in HBet5; spliter. apply inter_uniquenessH with D B C E; Col; try exists lBD; auto. intro; apply HNC1; ColHR. } apply between_only_one' in HBet5; spliter; intuition. } } { destruct HCut4 as [_ [_ [I [HI5 HBet4]]]]. assert (I = C); [|subst]. { apply betH_expand in HBet1; apply betH_expand in HBet2; apply betH_expand in HBet3; apply betH_expand in HBet4; spliter. apply inter_uniquenessH with G E F C; Col; try exists lCF; auto. intro; apply HNC4; ColHR. } apply between_only_one' in HBet4; spliter; intuition. } } 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