proposition: Lemma cut2_not_cut : forall A B C l, ~ColH A B C -> cut l A B -> cut l A C -> ~cut l B C.
proof: Proof. intros. unfold cut in *. intro. spliter. destruct H8 as [AB Hab]. destruct H6 as [AC Hac]. destruct H4 as [BC Hbc]. spliter. assert(ColH A AB B /\ ColH A AC C /\ ColH B BC C). repeat split. apply between_col in H11. tauto. apply between_col in H9. tauto. apply between_col in H6. tauto. spliter. assert(ColH AB AC BC). line_col AB AC BC. assert(AB <> AC /\ AB <> BC /\ AC <> BC). { apply betH_distincts in H11. apply betH_distincts in H9. apply betH_distincts in H6. spliter. repeat split; intro; apply H. subst AC. apply(colH_trans A AB); Col. subst BC. apply(colH_trans B AB); Col. subst BC. apply(colH_trans C AC); Col. } spliter. assert(HH:=between_one AB AC BC H16 H17 H18 H15). assert(HH12:= H11). assert(HH10:= H9). assert(HH7:=H6). apply betH_distincts in HH12. apply betH_distincts in HH10. apply betH_distincts in HH7. spliter. induction HH. line A C m H24. assert(~ ColH AB BC B). { intro. apply H. assert(ColH A B BC). apply(colH_trans B AB); Col. apply(colH_trans B BC); Col. } assert(~ IncidL B m). intro. apply H. line_col A B C. assert(cut m AB BC). unfold cut. repeat split. intro. apply H. apply(colH_trans A AB); Col. line_col A AB C. intro. apply H. line_col A C BC. apply(colH_trans C BC); Col. exists AC. split. col_line H13 m0. lines_eq m m0. assumption. assumption. destruct (plane_existence AB BC B H31) as [p]. spliter. assert(HH:= pasch AB BC B m p). induction HH; trivial. clear dependent p. unfold cut in H37. spliter. destruct H36 as [I H36]. spliter. assert(HH37:= H37). apply between_col in HH37. spliter. apply H. assert(ColH A I B). apply(colH_trans B AB); Col. assert(ColH A I C). line_col A I C. apply (colH_trans A I); Col. intro. subst I. apply between_only_one' in H37. tauto. clear dependent p. unfold cut in H37. spliter. destruct H36 as [C' H36]. spliter. assert(HH38:=H37). apply between_col in HH38. spliter. assert(ColH B C C'). apply(colH_trans B BC); Col. assert(C <> C'). intro. subst C'. unfold cut in H33. spliter. destruct H40 as [I H42]. spliter. assert(I = AC). apply(inter_uniquenessH A C AB BC); Col. intro. apply H. apply (colH_trans A AB); Col. line_col A C I. apply between_col in H41. spliter. Col. subst I. clean_duplicated_hyps. apply between_only_one' in H37. spliter. apply between_comm in H6. tauto. apply H. apply (colH_trans C C'); Col. line_col C C' A. apply (line_on_plane A C); trivial. apply (line_on_plane' AB B); Col. apply (line_on_plane' B BC); Col. induction H28. line C B m (sym_not_equal H21). assert(~ ColH AB AC A). intro. apply H. assert(ColH A C AB). apply(colH_trans A AC); Col. apply(colH_trans A AB); Col. assert(~ IncidL A m). intro. apply H. line_col A B C. assert(cut m AC AB). unfold cut. repeat split. intro. apply H. apply(colH_trans C AC); Col. line_col C AC B. intro. apply H. line_col B C AB. apply(colH_trans B AB); Col. exists BC. split. col_line H14 m0. lines_eq m m0. assumption. assumption. apply cut_comm in H33. destruct (plane_existence AB AC A H31) as [p]. spliter. assert(HH:= pasch AB AC A m p). induction HH; trivial. clear dependent p. unfold cut in H37. spliter. destruct H36 as [B' H36]. spliter. assert(HH38:=H37). apply between_col in HH38. spliter. assert(ColH A B B'). apply(colH_trans A AB); Col. assert(B <> B'). intro. subst B'. unfold cut in H33. spliter. destruct H40 as [I H42]. spliter. assert(I = BC). apply(inter_uniquenessH C B AC AB); Col. intro. apply H. apply (colH_trans C AC); Col. line_col C B I. apply between_col in H41. spliter. Col. subst I. apply between_only_one' in H37. spliter. apply between_comm in H11. tauto. apply H. apply (colH_trans B B'); Col. line_col B B' C. clear dependent p. unfold cut in H37. spliter. destruct H36 as [I H36]. spliter. assert(HH38:= H37). apply between_col in HH38. spliter. apply H. assert(ColH C I A). apply(colH_trans A AC); Col. assert(ColH C I B). line_col C I B. apply (colH_trans C I); Col. intro. subst I. apply between_only_one' in H37. spliter. apply between_comm in H9. tauto. apply (line_on_plane B C); trivial. apply (line_on_plane' A AB); Col. apply (line_on_plane' A AC); Col. line A B m H27. assert(~ ColH BC AC C). intro. apply H. assert(ColH B C AC). apply(colH_trans C BC); Col. apply(colH_trans C AC); Col. assert(~ IncidL C m). intro. apply H. line_col A B C. assert(cut m BC AC). unfold cut. repeat split. intro. apply H. apply(colH_trans B BC); Col. line_col B BC A. intro. apply H. line_col B A AC. apply(colH_trans A AC); Col. exists AB. split. col_line H12 m0. lines_eq m m0. assumption. apply between_comm. assumption. destruct (plane_existence BC AC C H31) as [p]. spliter. assert(HH:= pasch BC AC C m p). induction HH; trivial. clear dependent p. unfold cut in H37. spliter. destruct H36 as [I H36]. spliter. assert(HH38:= H37). apply between_col in HH38. spliter. apply H. assert(ColH B I C). apply(colH_trans C BC); Col. assert(ColH B I A). line_col B I A. apply (colH_trans B I); Col. intro. subst I. apply between_only_one' in H37. tauto. clear dependent p. unfold cut in H37. spliter. destruct H36 as [A' H36]. spliter. assert(HH38:=H37). apply between_col in HH38. spliter. assert(ColH C A A'). apply(colH_trans C AC); Col. assert(A <> A'). intro. subst A'. unfold cut in H33. spliter. destruct H40 as [I H42]. spliter. assert(I = AB). apply(inter_uniquenessH B A BC AC); Col. intro. apply H. apply (colH_trans B BC); Col. line_col B A I. apply between_col in H41. spliter. Col. subst I. clean_duplicated_hyps. apply between_only_one' in H37. spliter. tauto. apply H. apply (colH_trans A A'); Col. line_col A A' B. apply (line_on_plane A B); trivial. apply (line_on_plane' AC C); Col. destruct H14 as [n]; spliter. apply (line_on_plane' BC C); 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