proposition: Lemma OS2__TS : forall O X Y Z, same_side' Y Z O X -> same_side' X Y O Z -> cut' X Z O Y.
proof: Proof. intros O X Y Z HOS1 HOS2. destruct (between_out Z O) as [Z' HZ']; [unfold same_side' in *; spliter; auto|]. assert (HTS : cut' Y Z' O X). { assert (HD1 : O <> X) by (unfold same_side' in *; spliter; auto). assert (HD2 : O <> Z) by (unfold same_side' in *; spliter; auto). split; [auto|intro l; intros]. apply cut_comm; apply cut_same_side_cut with Z; [|destruct HOS1 as [_ HOS1]; apply same_side_comm; apply HOS1; auto]. destruct (same_side_not_incid Y Z l) as [HNI1 HNI2]; [destruct HOS1 as [_ HOS1]; apply HOS1; auto|]. assert (HNC := IncidL_not_IncidL__not_colH O X Z l HD1). split; [|split; auto; exists O; split; try apply between_comm; auto]. intro; apply HNC; auto. assert (HC1 : ColH O X Z') by (exists l; auto). assert (HD3 := betH_distincts _ _ _ HZ'); spliter. assert (HC2 := between_col _ _ _ HZ'); ColHR. } split; [destruct (same_side_prime_not_colH _ _ _ _ HOS1) as [HNC _]; intro; subst; apply HNC; Col|intro l; intros]. apply cut_comm; apply cut_same_side_cut with Z'. { assert (HD1 : O <> X) by (unfold same_side' in *; spliter; auto). assert (HD2 : O <> Z) by (unfold same_side' in *; spliter; auto). destruct (same_side_prime_not_colH _ _ _ _ HOS2) as [_ HNC]. split; [intro; apply HNC; exists l; auto|]. assert (HD3 : O <> Y) by (intro; subst; apply HNC; Col). split; [intro|exists O; auto]. assert (HD4 := betH_distincts _ _ _ HZ'); spliter. assert (HC1 : ColH O Y Z') by (exists l; auto). assert (HC2 := between_col _ _ _ HZ'). apply HNC; apply between_col in HZ'; ColHR. } { destruct HTS as [HD1 HTS]; line O X m HD1. assert (HCut : cut m Y Z') by (apply HTS; auto). assert (HX' := HCut); destruct HX' as [HNI1 [HNI2 [X' [HI HBet]]]]. apply same_side_trans with X'. { apply out_same_side with Y; try (right; left); auto. destruct (same_side_prime_not_colH _ _ _ _ HOS2) as [_ HNC]. intro; assert (HC1 : ColH O Y Z') by (exists l; auto). assert (HD3 := betH_distincts _ _ _ HZ'); spliter. assert (HC2 := between_col _ _ _ HZ'). apply HNC; apply between_col in HZ'; ColHR. } { assert (HC : ColH O X X') by (exists m; auto). destruct (same_side_prime_not_colH _ _ _ _ HOS1) as [HNC1 _]. apply same_side_comm; apply out_same_side with O; auto; [intro; apply HNC1; exists l; auto|]. elim (eq_dec_pointsH X X'); intro HD2; [subst; apply outH_trivial; auto|]. destruct (same_side_prime_not_colH _ _ _ _ HOS2) as [_ HNC2]. assert (HD3 := betH_distincts _ _ _ HZ'); spliter. assert (HC2 := between_col _ _ _ HZ'). assert (HC3 := between_col _ _ _ HBet). elim (eq_dec_pointsH O X'); intro HD3; [subst; exfalso; apply HNC2; ColHR|]. assert (HC4 := HC); apply between_one in HC; auto. elim HC; clear HC; intro HC; [left; auto|]. elim HC; clear HC; intro HFalse; [right; left; apply between_comm; auto|]. assert (HD4 : O <> Z) by auto; line O Z o HD4. assert (HOS3 : same_side X Y o) by (destruct HOS2 as [_ HOS]; apply HOS; auto). exfalso; apply (same_side_not_cut _ _ _ HOS3). apply cut_same_side_cut with X'. { destruct (same_side_prime_not_colH _ _ _ _ HOS1) as [_ HNC3]. split; [intro; apply HNC3; exists o; auto|]. split;[|exists O; auto]. intro; assert (ColH X' O Z) by (exists o; auto); apply HNC3; ColHR. } { apply out_same_side with Z'; try (left; apply between_comm; auto). { destruct HC2 as [p [HI' ]]; spliter. apply (line_uniqueness _ O o) in HI'; auto; rewrite HI'; auto. } { intro; assert (ColH O X' Z) by (exists o; auto). destruct (same_side_prime_not_colH _ _ _ _ HOS2) as [HNC3 _]. apply HNC3; ColHR. } } } } 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