proposition: Lemma l11_62_existence : forall A B C P, exists D, Coplanar A B C D /\ forall E, Coplanar A B C E -> Per E D P.
proof: Proof. intros A B C P. destruct (cop_dec A B C P) as [|HNCop]. exists P; split; [assumption|intros; Perp]. assert (HNCol : ~ Col A B C) by (apply ncop__ncol with P, HNCop). destruct (l8_18_existence A B P) as [D0 [HCol0 HPerp0]]. intro; apply HNCop; exists P; left; split; Col. assert (HCop0 : Coplanar A B C D0) by (exists D0; left; split; Col). assert_diffs. destruct (ex_perp_cop A B D0 C) as [D1 [HPerp1 HCop1]]; auto. destruct (perp_not_col2 A B D1 D0 HPerp1) as [HNCol1|]; [|exfalso; Col]. assert (Haux : forall D, Col D0 D1 D -> Coplanar A B C D). { intros D HD. apply coplanar_trans_1 with D1; [Col|Cop|]. assert_diffs; apply coplanar_perm_12, col_cop__cop with D0; Col; Cop. } destruct (diff_col_ex3 A B D0 HCol0) as [A0]. spliter. assert (HCopA : Coplanar A B C A0) by (exists A0; left; split; Col). assert (Per P D0 A0) by (destruct (l8_16_1 A B P A0 D0); auto). destruct (per_dec P D0 D1) as [|HNPer]. { exists D0. split; Col. intros E HE. apply l11_60 with A0 D1 D0; Perp. intro; apply HNCol1; ColR. apply coplanar_pseudo_trans with A B C; trivial. } destruct (l8_18_existence D0 D1 P) as [D []]; Col. intro Habs; apply HNCop, Haux, Habs. exists D; split; auto. intros E HE. assert (D <> D0) by (intro; subst; apply HNPer; Perp). assert (HPer : Per D0 D P) by (apply perp_per_1, perp_left_comm, perp_col with D1; auto). assert (HPer1 : Per D D0 A0). assert_diffs; apply l8_2, per_col with D1; auto; destruct (l8_16_1 A B D1 A0 D0); Perp. apply l11_60 with D0 A0 D; Perp; [apply per_not_col in HPer1; Col|..]. { destruct (symmetric_point_construction A0 D) as [A0']. apply l8_2; exists A0'; split; trivial. destruct (symmetric_point_construction D0 D) as [D0']. apply l10_12 with D0 D0'; [..|apply per_double_cong with D|apply cong_symmetry, l7_13 with D]; Perp. destruct (symmetric_point_construction P D) as [P']. apply midpoint_preserves_per with P' D0 A0 D; Midpoint. apply l11_60 with P D D0; Perp; [|exists P'; left; split; Col]. intro; apply HNCop, coplanar_trans_1 with D1; Col; [Cop|]. exists D0; right; right; split; ColR. } apply coplanar_pseudo_trans with A B C; trivial. apply coplanar_trans_1 with D1; Col. Cop. exists D0; right; right; split; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2