proposition: Lemma lta_os__ts : forall A O B P, ~ Col A O P -> LtA A O P A O B -> OS O A B P -> TS O P A B.
proof: Proof. intros. unfold LtA in *. spliter. unfold LeA in *. ex_and H0 P'. assert(~Col A O B). { unfold OS in H1. ex_and H1 R. unfold TS in H1. spliter; Col. } unfold TS. repeat split; Col. intro. induction H5. assert(TS O A B P). { repeat split; Col. exists O. split; Col. } apply l9_9 in H6. contradiction. apply H2. assert_diffs. apply out2__conga. apply out_trivial; auto. repeat split; auto. induction H5. right; Between. left; auto. Between. unfold InAngle in *. spliter. ex_and H7 T. exists T. split; auto. induction H8. treat_equalities; Col. assert(HCop : Coplanar A O P P'). { apply coplanar_trans_1 with B; Col. Cop. exists T. left. split; Col. } assert(HH:= conga_cop__or_out_ts A O P P' HCop H3). induction HH. assert(Out O P T) by (apply (l6_7) with P'; finish). Col. exfalso. assert(A <> T). { intro. treat_equalities. unfold TS in H9. spliter. apply H9. Col. } assert(OS O A T P'). { apply out_one_side. left. intro. apply H4. ColR. auto. } assert(OS A O B T). { apply out_one_side. left; Col. repeat split; auto. intro. treat_equalities. apply H4; Col. } assert(OS O A B P'). { apply (one_side_transitivity _ _ _ T); Side. } assert(TS O A B P) by (apply(l9_8_2 _ _ P'); Side). apply l9_9 in H14. contradiction. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2