proposition: Lemma l9_19 : forall X Y A B P , Col X Y P -> Col A B P -> (OS X Y A B <-> (Out P A B /\ ~Col X Y A)).
proof: Proof. intros. split. intro. assert (HH2:=H1). unfold OS in H1. ex_and H1 D. unfold TS in H2. assert (~ Col B X Y). spliter. assumption. spliter. clear H3. assert (X <> Y). intro. subst Y. spliter. Col. unfold TS in H1. spliter. ex_and H5 M. ex_and H7 N. split. unfold Out. repeat split. intro. subst P. apply H1. apply col_permutation_2. assumption. intro. subst P. apply H2. apply col_permutation_2. assumption. unfold Col in H0. induction H0. right. apply between_symmetry. assumption. induction H0. apply False_ind. assert (TS X Y A B). unfold TS. repeat split. assumption. assumption. exists P. split. apply col_permutation_2. assumption. apply between_symmetry. assumption. apply l9_9_bis in HH2. contradiction. left. assumption. intro. apply H1. Col. intros. spliter. assert (exists D, TS X Y A D). apply l9_10. intro. apply H2. apply col_permutation_1. assumption. ex_elim H3 D. unfold OS. exists D. split. assumption. eapply l9_5. apply H4. apply col_permutation_2. apply H. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar