proposition: Lemma l13_10_aux4 : 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 -> Bet O A B -> Out O A' B'.
proof: Proof. intros. assert(A <> O). intro. subst A. apply H. Col. assert(A' <> O). intro. subst A'. apply H. Col. assert(Col O A C). ColR. induction(eq_dec_points A B). subst B. assert (HH : Par C A' C B'). assert(~ Col A C' O). intro. apply H. ColR. assert(HH:= perp2_pseudo_trans C A' A C' C B' O H9 H8 H14). ex_and HH X. ex_and H15 Y. apply (l12_9 _ _ _ _ X Y); Perp. Cop. Cop. Cop. exists O. left. split; Col. assert(A' = B'). assert(Col A' B' C). induction HH. apply False_ind. apply H14. exists C. split; Col. spliter. Col. apply (l6_21 O C' C B'); Col. intro. apply H. ColR. intro. subst B'. apply par_distinct in HH. tauto. ColR. subst B'. apply out_trivial. auto. assert(Bet C O A \/ Bet O C A \/ Bet A C B \/ Bet A B C). apply(fourth_point O A B C); auto. induction H15. assert(Bet B' O C'). assert(Bet C O B). apply outer_transitivity_between with A; auto. apply(perp2_preserves_bet13 O B C B' C'); Between. intro. apply H. ColR. assert(Bet A' O C'). apply(perp2_preserves_bet13 O A C A' C');Between. ColR. apply perp2_sym. assumption. repeat split; auto. apply(l5_2 C' O A' B'); Between. induction H15. assert(Bet O C B). apply between_exchange4 with A; assumption. assert(Bet O B' C'). apply(perp2_preserves_bet23 O C B B' C'); Col. intro. apply H. ColR. apply perp2_sym. auto. assert(Bet O A' C'). apply(perp2_preserves_bet23 O C A A' C'); Between. ColR. intro. apply H. ColR. repeat split; auto. apply(l5_3 O A' B' C'); auto. induction H15. assert(Bet O A C). apply between_inner_transitivity with B; assumption. assert(Bet O C' A'). apply(perp2_preserves_bet23 O A C C' A'); auto. ColR. intro. apply H. ColR. apply perp2_sym. auto. assert(Bet O C B). apply between_exchange2 with A; assumption. assert(Bet O B' C'). apply(perp2_preserves_bet23 O C B B' C'); auto. intro. apply H. ColR. apply perp2_sym. auto. repeat split; auto. right. apply between_exchange4 with C'; assumption. assert(Bet O A C). apply outer_transitivity_between with B; auto. assert( Bet O B C). apply between_exchange2 with A; assumption. assert(Bet O C' B'). apply(perp2_preserves_bet23 O B C C' B'); Col. intro. apply H. ColR. assert(Bet O C' A'). apply(perp2_preserves_bet23 O A C C' A'); auto. ColR. intro. apply H. ColR. apply perp2_sym. auto. repeat split; auto. apply (l5_1 _ C'); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_4_cos GeoCoq.Tarski_dev.Annexes.project