proposition: Lemma coplanar_plane0 : forall A B C D X, ColH A B X -> ColH C D X -> exists p, IncidP A p /\ IncidP B p /\ IncidP C p /\ IncidP D p.
proof: Proof. intros A B C D X [l] [m]; spliter. destruct (other_point_on_line X l) as [Y [HXY ]]; [assumption|]. destruct (EqL_dec l m) as [Heq|Hneq]. rewrite <- Heq in *. destruct (ncolH_exists X Y HXY) as [Z HNCol]. destruct (plane_existence X Y Z HNCol) as [p]; spliter. assert (Hlp : IncidLP l p) by (apply (line_on_plane X Y); assumption). exists p; repeat split; auto. destruct (other_point_on_line X m) as [Z [HXZ ]]; [assumption|]. assert (HNCol : ~ ColH X Y Z). apply IncidL_not_IncidL__not_colH with l; [assumption..|]. intro; apply Hneq, (line_uniqueness X Z); assumption. destruct (plane_existence X Y Z HNCol) as [p]; spliter. assert (Hlp : IncidLP l p) by (apply (line_on_plane X Y); assumption). assert (Hmp : IncidLP m p) by (apply (line_on_plane X Z); assumption). exists p; repeat split; 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