proposition: Lemma l8_21_bis : forall A B C X Y, X <> Y -> ~ Col C A B -> exists P : Tpoint, Cong A P X Y /\ Perp A B P A /\ TS A B C P.
proof: Proof. intros. assert (A <> B) by (intro; subst; Col). assert(HH:= l8_21 A B C H1). ex_and HH P. ex_and H2 T. assert(TS A B C P). unfold TS. repeat split; auto. intro. apply perp_not_col in H2. apply H2. Col. exists T. split; Col. assert(P <> A). apply perp_distinct in H2. tauto. assert(HH:= segment_construction_2 P A X Y H6). ex_and HH P'. exists P'. assert(Perp A B P' A). apply perp_sym. apply perp_left_comm. apply (perp_col _ P). intro. subst P'. apply cong_symmetry in H8. apply cong_identity in H8. contradiction. Perp. induction H7. apply bet_col in H7. Col. apply bet_col in H7. Col. repeat split;auto. apply perp_not_col in H9. intro. apply H9. Col. assert(OS A B P P'). apply out_one_side. left. apply perp_not_col in H2. assumption. repeat split; auto. apply perp_distinct in H9. tauto. assert(TS A B C P'). apply l9_2. apply(l9_8_2 A B P P' C); auto. apply l9_2. assumption. unfold TS in H11. spliter. ex_and H13 T'. exists T'. split; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar