proposition: Lemma l13_10_aux5 : forall A B C A' B' C' O, ~ Col O A A' -> B <> O -> C <> O -> Col O A B -> Col O B C -> B' <> O -> C' <> O -> Col O A' B' -> Col O B' C'-> Perp2 B C' C B' O -> Perp2 C A' A C' O -> Out O A B -> Out O A' B'.
proof: Proof. intros. assert(A' <> O). intro. subst A'. apply H. Col. induction H10. spliter. induction H13. eapply (l13_10_aux4 A B C _ _ C'); auto. apply l6_6. apply(l13_10_aux4 B A C B' A' C'); try assumption. intro. apply H. ColR. Col. ColR. Col. ColR. apply perp2_sym. assumption. apply perp2_sym. auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_4_cos GeoCoq.Tarski_dev.Annexes.project