proposition: Lemma per3_preserves_bet2_aux : forall O A B C B' C', Col O A C -> A <> C' -> Bet A B' C' -> O <> A -> O <> B' -> O <> C' -> Per O B' B -> Per O C' C -> Col A B C -> Col O A C' -> Bet A B C.
proof: Proof. intros O A B C B' C'. intro HX. intros. induction(eq_dec_points A B). subst B. Between. induction(eq_dec_points B C). subst C. Between. assert(Col O A B'). apply bet_col in H0. ColR. assert(Col O B' C'). apply bet_col in H0. ColR. induction(eq_dec_points B B'). subst B'. assert(Col O C C'). apply bet_col in H0. ColR. assert(C = C'). apply(per_col_eq C C' O); Col; Perp. subst C'. assumption. assert(C <> C'). intro. subst C'. apply per_not_col in H4; auto. apply H4. ColR. assert(Perp O A C C'). apply per_perp_in in H5; auto. apply perp_in_comm in H5. apply perp_in_perp_bis in H5. induction H5. apply (perp_col _ C'); Col; Perp. apply perp_distinct in H5. tauto. assert(Perp O A B B'). apply per_perp_in in H4; auto. apply perp_in_comm in H4. apply perp_in_perp_bis in H4. induction H4. apply (perp_col _ B'); Col; Perp. apply perp_distinct in H4. tauto. assert(Par B B' C C'). apply(l12_9 B B' C C' O A); [Cop..|Perp|Perp]. induction H16. assert(HH:=l12_6 B B' C C' H16). assert(TS B B' A C'). repeat split. intro. assert(Per B B' A). apply(per_col B B' O A); Col; Perp. apply per_not_col in H18; auto. apply H18. Col. intro. subst B'. clean_trivial_hyps. apply H16. exists C. split; Col. intro. apply H16. exists C'. split; Col. exists B'. split; Col. assert(TS B B' C A). apply(l9_8_2 B B' C' C A). apply l9_2; auto. apply one_side_symmetry; auto. unfold TS in H18. spliter. ex_and H20 T. assert(B = T). apply (l6_21 A C B' B); Col. assert(A <> C). intro. subst C. apply between_identity in H21. subst T. contradiction. intro. apply bet_col in H0. apply H19. ColR. subst T. Between. spliter. assert(B' <> C'). intro. subst C'. clean_trivial_hyps. assert(Perp O B' C B'). apply(perp_col O A C B' B'); Col. apply perp_left_comm in H0. apply perp_not_col in H0. apply H0. ColR. assert(Per C C' B'). apply(per_col C C' O B'); Col; Perp. apply per_not_col in H21; auto. apply False_ind. apply H21. Col. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel