proposition: Lemma plane_separation : forall A B X Y p, ~ ColH A X Y -> ~ ColH B X Y -> IncidP A p -> IncidP B p -> IncidP X p -> IncidP Y p -> cut' A B X Y \/ same_side' A B X Y.
proof: Proof. intros A B X Y p HNC1 HNC2 HAp HBp HXp HYp; assert (HD1 : X <> Y) by (intro; subst; Col). line X Y l HD1; destruct (cut_exists A l) as [C HC1]; [intro; apply HNC1; exists l; auto|]. elim (eq_dec_pointsH A B); [intro; subst; right; apply same_side_prime_refl; intro; apply HNC1; Col|intro HD2]. assert (HD3 : A <> C) by (apply cut_distinct with l; auto). elim (eq_dec_pointsH B C). { intro; subst; left; split; auto; intro m; intros. destruct HC1 as [HNI1 [HNI2 [I [HI HBet]]]]. split; [apply (line_uniqueness _ Y m l) in H; try rewrite H; auto|]. split; [apply (line_uniqueness _ Y m l) in H; try rewrite H; auto|]. exists I; split; auto; apply (line_uniqueness _ Y m l) in H; auto; rewrite H; auto. } { intro HD4; elim (colH_dec A C B). { intro HCol1; assert (HI := HC1); destruct HI as [_ [_ [I [HInc HCol2]]]]. apply between_col in HCol2; assert (HE : ColH A I B) by ColHR. apply between_one in HE; auto; [|intro; subst; apply HNC1|intro; subst; apply HNC2]; try exists l; auto. assert (HNI : ~ IncidL A l) by (intro; apply HNC1; exists l; auto). elim HE; clear HE; intro HE; try (elim HE; clear HE; intro HE); [left|right; split; auto; intro m; intros; apply (line_uniqueness _ Y m l) in H; try rewrite H in *; auto; apply out_same_side with I; unfold outH; auto..]. split; [intro; subst; Col|intro m; intros]. split; [intro; apply HNC1; exists m; auto|]. split; [intro; apply HNC2; exists m; auto|]. exists I; split; auto. apply (line_uniqueness _ Y m l) in H; try rewrite H; auto. } { assert (IncidLP l p) by (apply (line_on_plane X Y); trivial). assert (IncidP C p). { destruct HC1 as [_ [_ [I [ HI1 HI2]]]]. apply betH_colH in HI2; spliter. apply (line_on_plane' A I); trivial. apply (line_on_plane X Y l); assumption. } intro HNC3; elim (pasch A C B l p); auto; intro HC2; try (apply HNC2; exists l; auto); [left|right]; split; auto; intro m; intros; apply (line_uniqueness _ Y m l) in H; try rewrite H; try (exists C; split); auto; apply cut_comm; auto. } } 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