proposition: Lemma l13_10_aux3 : 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 A O B -> Bet A' O 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). apply (col_transitivity_1 _ B); Col. assert(Col O A' C'). apply (col_transitivity_1 _ B'); Col. assert(Bet C A O \/ Bet A C O \/ Bet O C B \/ Bet O B C). apply(fourth_point A O B C); auto. ColR. induction H15. assert(Bet O C' A'). apply(perp2_preserves_bet23 O A C C' A'); Between. Col. intro. apply H. ColR. apply perp2_sym. auto. assert(Bet B' O C'). apply(perp2_preserves_bet13 O B C B' C'); auto. apply outer_transitivity_between with A; Between. intro. apply H. ColR. apply between_symmetry, outer_transitivity_between with C'; auto. induction H15. assert(Bet C O B). apply (between_exchange3 A); assumption. assert(Bet O A' C'). apply(perp2_preserves_bet23 O C A A' C'); Between. intro. apply H. ColR. assert(Bet B' O C'). apply(perp2_preserves_bet13 O B C B' C'); Between. intro. apply H. ColR. apply (between_exchange3 C'); Between. induction H15. assert(Bet A O C). apply between_inner_transitivity with B; assumption. assert(Bet O B' C'). apply(perp2_preserves_bet23 O C B B' C'); Between. intro. apply H. ColR. apply perp2_sym. auto. assert(Bet C' O A'). apply(perp2_preserves_bet13 O C A C' A'); Col. Between. intro. apply H. ColR. apply between_inner_transitivity with C'; Between. assert(Bet A O C). apply outer_transitivity_between with B; auto. assert(Bet O C' B'). apply(perp2_preserves_bet23 O B C C' B'); Col. intro. apply H. ColR. assert(Bet C' O A'). apply(perp2_preserves_bet13 O C A C' A'); Col. Between. intro. apply H. ColR. apply outer_transitivity_between with C'; Between. Qed.
imports: GeoCoq.Tarski_dev.Ch13_4_cos GeoCoq.Tarski_dev.Annexes.project