proposition: Lemma betH_trans0 : forall A B C D, BetH A B C -> BetH A C D -> BetH B C D /\ BetH A B D.
proof: Proof. intros. apply betH_expand in H. apply betH_expand in H0. spliter. clean_duplicated_hyps. assert(HH:=ncolH_exists A B H5). destruct HH as [G HE]. assert(B <> G). apply ncolH_distincts in HE. tauto. assert(HF:=between_out B G H1). ex_and HF F. apply betH_expand in H9. spliter. elim (eq_dec_pointsH C F). intros HCF. subst. exfalso. apply HE. apply (colH_trans B F);Col. intro HCF. line C F l HCF. assert(~cut l A B). intro. unfold cut in H16. spliter. ex_and H18 X. assert(X=C). apply (inter_uniquenessH A B F C); Col. intro. apply HE. apply(colH_trans B F); Col. apply between_col in H19. spliter; Col. line_col F C X. subst X. apply between_only_one in H19. spliter. apply between_comm in H. contradiction. assert(~cut l B G). intro. unfold cut in H17. spliter. ex_and H19 X. apply betH_expand in H20. spliter. assert(ColH B X F). apply (colH_trans B G); Col. col_line H25 l00. assert(X <> F). intro. subst X. apply between_only_one in H20. spliter. apply between_comm in H9. contradiction. lines_eq l l00. contradiction. assert(~cut l A G). destruct (plane_existence A B G HE) as [p]. spliter. apply not_cut3 with B p; trivial. apply (line_on_plane C F); trivial. apply (line_on_plane' A B); Col. apply (line_on_plane' B G); Col. intro. assert(ColH B C G). apply (colH_trans B F);Col. line_col B F C. apply HE. apply (colH_trans B C); Col. intro. apply HE; Col. intro. apply cut_comm in H21. contradiction. assert(cut l A G \/ cut l D G). assert (~ ColH A D G). intro. apply HE. apply(colH_trans A D); Col. apply (colH_trans A C) ; Col. destruct (plane_existence A D G H19) as [p]. spliter. apply(pasch A D G l p); trivial. assert (IncidP C p). apply (line_on_plane' A D); Col. apply (line_on_plane C F); trivial. apply (line_on_plane' B G); Col. apply (line_on_plane' A C); Col. intro. assert(ColH B C G). apply (colH_trans G F); Col. line_col G F C. apply HE. apply (colH_trans B C); Col. unfold cut. repeat split. intro. assert(ColH A C F). line_col A C F. assert(ColH A B F). apply (colH_trans A C); Col. apply HE. apply (colH_trans B F); Col. intro. assert(ColH C D F). line_col C D F. assert(ColH A C F). apply (colH_trans C D); Col. assert(ColH A B F). apply (colH_trans A C); Col. apply HE. apply (colH_trans B F); Col. exists C. split; auto. induction H19. contradiction. assert(~ ColH D G B). intro. assert(ColH A B D). apply (colH_trans A C); Col. apply HE. apply (colH_trans B D); Col. intro. subst D. apply between_only_one in H0. spliter. apply between_comm in H. contradiction. assert(~ IncidL B l). intro. assert(ColH B C G). apply (colH_trans B F); Col. line_col B F C. apply HE. apply (colH_trans B C); Col. destruct (plane_existence D G B H20) as [p]. spliter. assert(HH:=pasch D G B l p). induction HH; trivial. clear dependent p. unfold cut in H25. spliter. ex_and H24 C'. assert(C = C'). assert(ColH C C' F). line_col C C' F. apply (inter_uniquenessH A B F C); Col. intro. apply HE. apply (colH_trans B F); Col. apply betH_expand in H25. spliter. apply (colH_trans B D); Col. apply (colH_trans A C); Col. subst C'. assert(BetH B C D). apply between_comm. assumption. split; auto. assert(HH:=betH_trans A B C D H H26). tauto. apply cut_comm in H25. contradiction. apply (line_on_plane C F); trivial. apply (line_on_plane' B D); trivial. apply between_comm in H0. intro; apply (between_only_one A B C); subst; assumption. apply (colH_trans A C); Col. apply (line_on_plane' B G); 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