proposition: Lemma betH_trans1 : forall A B C D, BetH A B C -> BetH B C D -> BetH A C D.
proof: Proof. intros. assert(HH0 := H). assert(HH1:= H0). apply betH_distincts in HH0. apply betH_distincts in HH1. spliter. clean_duplicated_hyps. assert(HH:=ncolH_exists A C H6). destruct HH as [E HE]. assert(C <> E). apply ncolH_distincts in HE. tauto. assert(HF:=between_out C E H1). destruct HF as [F HF]. assert(HHF:=HF). apply betH_distincts in HHF. spliter. assert(ColH A B C). apply between_col in H. tauto. assert(ColH B C D). apply between_col in H0. tauto. assert(ColH C E F). apply between_col in HF. tauto. assert(~ColH F C B). intro. assert(ColH C E B). apply (colH_trans C F); Col. apply HE. apply (colH_trans B C); Col. assert(exists X : Point, Bet B X F /\ Bet E X A). apply(inner_pasch_aux A F C B E H13). unfold Bet. left; assumption. unfold Bet. left; apply between_comm; assumption. destruct H14 as [G H14]. spliter. induction H14. induction H15. assert(HH15:=H14). apply between_col in HH15. assert(HH16:=H15). apply between_col in HH16. spliter. assert(~ColH D B G). intro. assert(ColH B D F). apply (colH_trans B G); Col. intro. subst G. apply HE. apply(colH_trans A B); Col. apply H13. apply(colH_trans B D); Col. line C E m H1. assert(~(cut m A G \/ cut m B G)). intro. induction H19. unfold cut in H19. spliter. ex_and H21 E'. assert(E = E'). apply (inter_uniquenessH A G C F E E'); Col. intro. assert(ColH B C G). apply (colH_trans A C); Col. apply H16. apply (colH_trans B C); Col. ex_and H12 m0. lines_eq m m0. line_col C F E'. subst E'. apply between_only_one in H22. tauto. unfold cut in H19. spliter. ex_and H21 F'. assert(F = F'). apply betH_distincts in H14. spliter. apply (inter_uniquenessH C E B G); Col. intro. apply HE. apply (colH_trans B C); Col. line_col C E F'. subst F'. apply between_only_one in H22. spliter. apply between_comm in H14. contradiction. assert(~ ColH B D G ). intro. apply H16. Col. assert(~IncidL G m). spliter. intro. assert(ColH C E G). unfold ColH. exists m; split; auto. apply betH_distincts in H15. spliter. apply HE. apply (colH_trans E G); Col. assert(cut m D B). unfold cut. split. intro. assert(ColH A C D). apply(colH_trans B C); Col. apply HE. apply(colH_trans C D); Col. line_col C D E. split. intro. apply HE. apply(colH_trans B C); Col. line_col B C E. exists C. split; auto. apply between_comm. assumption. apply cut_comm in H22. destruct (plane_existence B D G H20) as [p]. spliter. assert(HP:= pasch B D G m p). induction HP; trivial. apply False_ind. apply H19. right. assumption. clear dependent p. unfold cut in H26. spliter. destruct H25 as [HX H25]. spliter. assert(~ ColH G D A). intro. assert(ColH A B D). apply (colH_trans B C); Col. apply H20. apply (colH_trans A D); Col. intro. subst D. apply between_only_one' in H0. spliter. apply between_comm in H. contradiction. assert(~IncidL A m). intro. apply HE. line_col A C E. assert(cut m G D). unfold cut. repeat split; auto. exists HX. split; auto. apply between_comm. assumption. destruct (plane_existence G D A H27) as [p]. spliter. assert(HP:=pasch G D A m p). induction HP; trivial. apply False_ind. apply H19. left. apply cut_comm. assumption. clear dependent p. unfold cut in H33. spliter. ex_and H32 C'. assert(C'= C). apply(inter_uniquenessH A D E F); Col. intro. apply HE. assert(ColH A C D). apply (colH_trans B C); Col. apply (colH_trans A D); Col. intro. subst D. apply H27. Col. apply between_col in H33; spliter. Col. apply (colH_trans B C); Col. unfold ColH in H12. ex_and H12 m0. lines_eq m m0. line_col E F C'. subst C'. apply between_comm. assumption. apply (line_on_plane C E). assumption. assumption. assumption. assert (ColH A C D) by (apply (colH_trans B C); Col). apply (line_on_plane' A D); Col. intro; apply (between_only_one A B C); subst; assumption. apply betH_distincts in H15. spliter. apply (line_on_plane' G A); Col. assert (IncidP C p). apply betH_distincts in H0. spliter. apply (line_on_plane' B D); Col. apply (line_on_plane C E); trivial. apply (line_on_plane' C F); Col. apply betH_distincts in H14. spliter. apply (line_on_plane' B G); Col. induction H15. subst G. apply False_ind. apply between_col in H14. spliter. apply H13. apply (colH_trans E F); Col. subst G. apply False_ind. apply between_col in H14. spliter. apply H13. apply (colH_trans A B); Col. induction H14. induction H15. subst G. apply False_ind. apply between_col in H15. spliter. apply HE. apply(colH_trans A B); Col. subst G. induction H15. subst E. apply False_ind. apply H13. Col. subst B; tauto. subst G. induction H15. apply between_col in H14. spliter. apply False_ind. apply HE. apply (colH_trans E F); Col. induction H14. subst F. tauto. subst F. apply False_ind. apply H13. 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