proposition: Lemma l8_21_3 : forall A B C D X, Coplanar A B C D -> ~ Coplanar A B C X -> exists P T, Orth A B C D P /\ Coplanar A B C T /\ Bet X T P.
proof: Proof. intros A B C D X HD HX. destruct (l11_62_existence_bis A B C X HX) as [E HE]. destruct (eq_dec_points D E). { subst E. destruct (segment_construction X D D X) as [Y []]. exists Y, D; subst; repeat split; trivial. assert (D <> X) by (intro; subst; apply (HX HD)); assert_diffs. apply col_orth__orth with X; Col. exists D; assumption. } destruct (l11_63_aux A B C D E X) as [P' [HOS HP']]; auto. destruct HE as [HNCol [HEX [HE [_ HOrth]]]]. assert (HOrth' : Orth_at D A B C D P') by (apply col_cop_orth__orth_at; Col). assert (HDP' : D <> P') by (apply orth_distincts in HP'; spliter; auto). assert (HNCop : ~ Coplanar A B C P'). apply orth_at__ncop2 with D D; auto; apply col_cop_orth__orth_at; Col. destruct HOrth' as [_ [_ [_ [_ HOrth']]]]. destruct (segment_construction P' D D P') as [P []]. assert (HT : TS D E X P). { apply l9_8_2 with P'; [|Side]. repeat split; [intro; apply HNCop, col_cop2__cop with D E; ColR..|exists D; split; Col]. } destruct HT as [_ [_ [T []]]]. exists P, T; repeat split; [|apply col_cop2__cop with D E; Col|assumption]. assert_diffs. apply col_orth__orth with P'; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2