proposition: Lemma l11_63_aux : forall A B C D E P, Coplanar A B C D -> D <> E -> Orth_at E A B C E P -> exists Q, OS D E P Q /\ Orth A B C D Q.
proof: Proof. intros A B C D E P HD HDE HOrth. assert (H' := HOrth). destruct H' as [HNCol [HEP [HE1 [_ HE2]]]]. assert (HNCop : ~ Coplanar A B C P). intro; apply HEP, (col_cop_orth_at__eq A B C E P); Col. destruct (l10_15 D E D P) as [Q [HQ1 HQ2]]; Col. intro; apply HNCop, col_cop2__cop with D E; auto. exists Q. split; [assumption|]. destruct (ex_ncol_cop A B C D E HDE) as [F [HF1 HF2]]. destruct (ex_perp_cop D E D F) as [D' [HD'1 HD'2]]; auto. assert (~ Col D' D E) by (assert_diffs; apply per_not_col; Perp). assert (Coplanar D E F A) by (apply coplanar_pseudo_trans with A B C; Cop). assert (Coplanar D E F B) by (apply coplanar_pseudo_trans with A B C; Cop). assert (Coplanar D E F C) by (apply coplanar_pseudo_trans with A B C; Cop). exists D. apply (cop3_orth_at__orth_at D' D E); [assumption|apply coplanar_pseudo_trans with D E F; Cop..|]. assert_diffs. apply l11_60_bis; Cop; [|Perp..]. destruct (ex_perp_cop D E E F) as [E' [HE'1 HE'2]]; auto. assert_diffs. apply (l11_61 E E' P); Perp. apply coplanar_trans_1 with F; Col; Cop. apply os__coplanar in HQ2; Cop. apply l8_2, HE2; Col. apply HE2; Col; apply coplanar_pseudo_trans with D E F; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2