proposition: Lemma l9_10 : forall P Q A, ~ Col A P Q -> exists C, TS P Q A C.
proof: Proof. intros. double A P A'. exists A'. unfold TS. repeat split. assumption. intro. apply H. eapply col_permutation_2. eapply (col_transitivity_1 _ A'). intro. subst A'. apply l7_2 in H0. eapply is_midpoint_id in H0. subst A. apply H. assumption. apply col_permutation_4. assumption. unfold Col. right; right. apply midpoint_bet. assumption. exists P. split. apply col_trivial_1. apply midpoint_bet. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar