proposition: Lemma os_ts1324__os : forall A X Y Z, OS A X Y Z -> TS A Y X Z -> OS A Z X Y.
proof: Proof. intros A X Y Z Hos Hts. destruct Hts as [HNColXY [HNColYZ [P [HColP HPBet]]]]. apply (one_side_transitivity _ _ _ P). - apply invert_one_side. apply one_side_symmetry. apply one_side_symmetry in Hos. apply one_side_not_col123 in Hos. apply out_one_side; Col. apply bet_out; Between; intro; subst Z; Col. - apply out_one_side. right; Col. apply (col_one_side_out _ X); Col. apply one_side_symmetry in Hos. apply (one_side_transitivity _ _ _ Z); auto. apply invert_one_side. apply one_side_not_col123 in Hos. apply out_one_side; Col. apply bet_out; auto; intro; subst X; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar