proposition: Lemma l9_17 : forall A B C P Q, OS P Q A C -> Bet A B C -> OS P Q A B.
proof: Proof. intros. induction (eq_dec_points A C). subst C. apply between_identity in H0. subst B. assumption. assert( HH:= H). unfold OS in H. ex_and H D. assert(HH1:=H). unfold TS in H2. assert (P <> Q). intro. subst Q. spliter. Col. spliter. unfold TS in H. assert (P <> Q). intro. subst Q. spliter. Col. spliter. ex_and H8 X. ex_and H5 Y. assert (exists T, Bet B T D /\ Bet X T Y). eapply l3_17. apply H9. apply H10. assumption. ex_and H11 T. unfold OS. exists D. split. assumption. unfold TS. repeat split. apply l9_9_bis in HH. intro. apply HH. unfold TS. repeat split. assumption. assumption. exists B. split. assumption. assumption. unfold TS in HH1. spliter. assumption. exists T. induction (col_dec A C D). assert (X = Y). apply l6_21 with P Q A D; Col. intro. subst D. assert (OS P Q A A). apply one_side_reflexivity. assumption. apply l9_9_bis in H14. contradiction. apply col_permutation_2. apply (col_transitivity_1 _ C). intro. subst D. apply between_identity in H10. subst Y. apply H4. assumption. Col. Col. subst Y. apply between_identity in H12. subst X. split. assumption. assumption. split. assert (X <> Y). intro. subst Y. apply between_identity in H12. subst X. apply H13. apply col_permutation_1. eapply (col_transitivity_1 _ T). intro. subst D. contradiction. unfold Col. left. apply between_symmetry. assumption. unfold Col. left. apply between_symmetry. assumption. apply col_permutation_2. apply (colx X Y); Col. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar