proposition: Lemma l9_31 : forall A X Y Z, OS A X Y Z -> OS A Z Y X -> TS A Y X Z.
proof: Proof. intros. assert(A <> X /\ A <> Z /\ ~ Col Y A X /\ ~ Col Z A X /\ ~Col Y A Z). unfold OS in *. ex_and H C. ex_and H0 D. unfold TS in *. spliter. split. intro. subst X. Col. split. intro. subst Z. Col. repeat split; assumption. spliter. prolong Z A Z' Z A. assert(Z' <> A). intro. subst Z'. apply cong_symmetry in H7. apply cong_identity in H7. subst Z. absurde. assert(TS A X Y Z'). eapply (l9_8_2 _ _ Z). unfold TS. repeat split. assumption. intro. apply H4. apply col_permutation_2. eapply (col_transitivity_1 _ Z'). auto. apply col_permutation_4. assumption. apply col_permutation_1. apply bet_col. assumption. exists A. split. apply col_trivial_1. assumption. apply one_side_symmetry. assumption. unfold TS in H9. assert (~ Col Y A X). spliter. assumption. spliter. ex_and H12 T. assert(T <> A). intro. subst T. apply H5. apply col_permutation_2. eapply (col_transitivity_1 _ Z'). auto. apply col_permutation_1. apply bet_col. assumption. apply col_permutation_1. apply bet_col. assumption. assert(OS Y A Z' T). eapply out_one_side. left. intro. apply H5. apply col_permutation_2. eapply (col_transitivity_1 _ Z'). auto. apply bet_col in H6. apply col_permutation_1. assumption. apply col_permutation_1. assumption. apply l6_6. apply bet_out. intro. subst T. contradiction. assumption. unfold Col in H12. induction H12. assert(OS Z' Z Y T). apply out_one_side. left. intro. apply H5. eapply col_permutation_1. eapply (col_transitivity_1 _ Z'). intro. subst Z'. apply between_identity in H6. subst Z. apply H4. apply col_trivial_1. apply col_permutation_4. assumption. apply bet_col in H6. apply col_permutation_5. assumption. apply l6_6. apply bet_out. intro. subst T. apply H11. apply bet_col. assumption. apply between_symmetry. assumption. assert(OS A Z Y T). apply invert_one_side. eapply (col_one_side _ Z'). apply bet_col in H6. apply col_permutation_5. assumption. auto. apply invert_one_side. assumption. assert(TS A Z X T). repeat split. intro. apply H11. apply col_permutation_2. eapply (col_transitivity_1 _ Z). assumption. apply col_permutation_1. assumption. apply bet_col in H6. apply col_permutation_4. assumption. unfold OS in H17. ex_and H17 C. unfold TS in H18. spliter. assumption. exists A. split. apply col_trivial_1. apply between_symmetry. assumption. assert(TS A Z Y X). eapply l9_8_2. eapply l9_2. apply H18. apply one_side_symmetry. assumption. apply l9_9 in H19. contradiction. assert(OS A Z T X). apply out_one_side. right. intro. apply H4. apply col_permutation_4. assumption. repeat split. assumption. auto. induction H12. right. assumption. left. apply between_symmetry. assumption. assert(TS A Y Z' Z). repeat split. unfold OS in H5. ex_and H15 C. unfold TS in H15. spliter. intro. apply H15. apply col_permutation_5. assumption. intro. apply H5. apply col_permutation_3. assumption. exists A. split. apply col_trivial_1. apply between_symmetry. assumption. assert(OS A Y T X). apply out_one_side. left. unfold OS in H15. ex_and H15 C. unfold TS in H18. spliter. intro. apply H18. apply col_permutation_3. assumption. repeat split. assumption. auto. induction H12. right. assumption. left. apply between_symmetry. assumption. apply invert_one_side in H15. assert (OS A Y Z' X). eapply one_side_transitivity. apply H15. assumption. eapply l9_8_2. apply H17. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar