proposition: Lemma os_out_os : forall A B C D C' P , Col A B P -> OS A B C D -> Out P C C' -> OS A B C' D.
proof: Proof. intros. assert(A <> B /\ ~ Col C A B). unfold OS in H0. ex_and H0 T. unfold TS in H0. spliter. split. intro. subst B. Col. assumption. spliter. prolong C P T C P. assert(P <> T). intro. subst T. treat_equalities. Col. assert(TS A B C T). unfold TS. repeat split; Col. intro. apply H3. assert_cols. ColR. exists P. split; Col. assert(TS A B T C'). apply bet_col in H4. eapply (out_out_two_sides _ _ T C _ _ P); Col. apply l9_2. assumption. apply out_trivial. auto. assert(OS A B C C'). eapply l9_8_1. apply H7. apply l9_2. assumption. eauto using one_side_transitivity, one_side_symmetry. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar