proposition: Lemma plane_coplanar : forall A B C D p, IncidP A p -> IncidP B p -> IncidP C p -> IncidP D p -> Coplanar A B C D.
proof: Proof. intros A B C D p HA HB HC HD. destruct (colH_dec A B C) as [HCol|HNCol]. apply col__coplanar, col_colh, HCol. assert (HAB : A <> B). intro; subst; apply HNCol; Col. assert (HM : exists M, Midpoint M A B). apply midpoint_existence. destruct HM as [M HM]. destruct (midpoint_distinct_1 M A B HAB HM). destruct HM. assert (HM : ColH A B M) by Col. destruct (eq_dec_pointsH D M) as [|HDM]. exists D; subst; left; split; Col. destruct (line_existence D M HDM) as [l []]. destruct (IncidL_dec A l). destruct HM as [m]; spliter. assert (Heq : hilbert_axioms.EqL m l) by (apply (line_uniqueness M A); auto). rewrite Heq in *. exists A; right; left; split; [|apply line_col with l]; Col. assert (~ IncidL B l). intro. destruct HM as [m]; spliter. assert (Heq : hilbert_axioms.EqL m l) by (apply (line_uniqueness M B); auto). rewrite Heq in *; auto. destruct (IncidL_dec C l). exists M; left; split; [Col|apply line_col with l; assumption]. assert (IncidP M p). apply (line_on_plane' A B); Col. destruct (pasch A B C l p) as [HI|HI]; trivial. - apply (line_on_plane D M); trivial. - repeat split; trivial; exists M; split; [|apply bet__beth]; auto. - destruct HI as [_ [_ [I []]]]. apply coplanar_trans_1 with I. rewrite col_colh; intro HCol; apply HNCol, (colH_trans A I); Col; intro; subst; auto. exists I; right; left; split; apply col_colh; Col. exists M; right; right; split; apply col_colh; [exists l|]; Col. - destruct HI as [_ [_ [I []]]]. apply coplanar_perm_6, coplanar_trans_1 with I. rewrite col_colh; intro HCol; apply HNCol, (colH_trans B I); Col; intro; subst; auto. exists I; right; left; split; apply col_colh; Col. exists M; right; right; split; apply col_colh; [exists l|]; 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