proposition: Lemma per23_preserves_bet : forall A B C B' C', Bet A B C -> A <> B' -> A <> C' -> Col A B' C' -> Per A B' B -> Per A C' C -> Bet A B' C'.
proof: Proof. intros. assert(HC:Col A B C). apply bet_col in H; Col. induction(eq_dec_points B B'). subst B'. assert(Col A C' C). ColR. assert(A = C' \/ C = C'). apply l8_9; auto. induction H6. contradiction. subst C'. assumption. assert(A <> C). intro. subst C. apply l8_8 in H4. contradiction. assert(C <> C'). intro. subst C'. assert(Col A B' B). ColR. assert(A = B' \/ B = B'). apply l8_9; auto. induction H8; contradiction. assert(Perp A B' B' B). apply per_perp_in in H3; auto. apply perp_in_comm in H3. apply perp_in_perp_bis in H3. induction H3; Perp. apply perp_distinct in H3. tauto. assert(Perp A C' C' C). apply per_perp_in in H4; auto. apply perp_in_comm in H4. apply perp_in_perp_bis in H4. induction H4; Perp. apply perp_distinct in H4. tauto. assert(Par B B' C C'). apply(l12_9 B B' C C' A B');Perp; Cop. apply perp_sym. apply(perp_col _ C'); Perp. ColR. induction(eq_dec_points B C). subst C. assert(B' = C'). apply(per2_col_eq A B' C' B); Perp. Col. subst C'. Between. assert(~Col A B' B). apply per_not_col in H3; auto. assert(~Col A C' C). apply per_not_col in H4; auto. assert(B' <> C'). intro. subst C'. clean_trivial_hyps. assert(Col B C B'). apply cop_per2__col with A; Perp. exists C; left; split; Col. apply H13; ColR. induction H10. apply l12_6 in H10. assert(TS B B' A C). repeat split;auto. intro. assert(A = B' \/ B = B'). apply l8_9; Col. induction H12; tauto. intro. apply H13; ColR. exists B. split; Col. assert(TS B B' A C'). apply l9_2. apply(l9_8_2 B B' C C' A); auto. apply l9_2. assumption. unfold TS in H16. spliter. ex_and H18 T. assert(T = B'). apply bet_col in H19. apply (l6_21 B B' A B'); Col. ColR. subst T. assumption. spliter. apply False_ind. apply H12. ColR. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel