proposition: Lemma per23_preserves_bet_inv : forall A B C B' C', Bet A B' C' -> A <> B' -> Col A B C -> Per A B' B -> Per A C' C -> Bet A B C.
proof: Proof. intros. induction(eq_dec_points B B'). subst B'. assert(Col A C' C). apply bet_col in H. ColR. assert(A = C' \/ C = C'). apply(l8_9 A C' C); auto. induction H5. subst C'. apply between_identity in H. contradiction. subst C'. assumption. assert(Perp A B' B' B). apply per_perp_in in H2. apply perp_in_comm in H2. apply perp_in_perp_bis in H2. induction H2. Perp. apply perp_distinct in H2. tauto. auto. auto. assert(Perp A C' C' C). apply per_perp_in in H3. apply perp_in_comm in H3. apply perp_in_perp_bis in H3. induction H3. Perp. apply perp_distinct in H3. tauto. intro. subst C'. apply between_identity in H. contradiction. intro. subst C'. induction(eq_dec_points A C). subst C. apply between_identity in H. contradiction. assert(Col A B' B). apply bet_col in H. ColR. assert(A = B' \/ B = B'). apply(l8_9 A B' B); auto. induction H8;contradiction. assert(Perp A B' C' C). apply bet_col in H. apply(perp_col _ C'); Col. assert( Par B' B C' C). apply(l12_9 B' B C' C A B'); Cop. Perp. Perp. induction(eq_dec_points B C). subst C. Between. induction H8. assert(B' <> C'). intro. subst C'. apply H8. exists B'. split; Col. assert(HH:=l12_6 B' B C' C H8). assert(TS B' B A C'). repeat split; auto. intro. assert(A = B' \/ B = B'). apply(l8_9 A B' B); auto. induction H12;contradiction. intro. assert(Col A B' B). assert_cols. ColR. assert(A = B' \/ B = B'). apply(l8_9 A B' B); auto. induction H13;contradiction. exists B'. split; Col. assert(TS B' B C A). apply(l9_8_2 B' B C' C A); auto. apply l9_2. assumption. unfold TS in H12. spliter. ex_and H14 T. assert(A <> C). intro. subst C. apply between_identity in H15. subst T. contradiction. assert (T = B). assert_cols. apply (l6_21 A C B' B); Col. intro. assert(Col A B' B). ColR. assert(A = B' \/ B = B'). apply(l8_9 A B' B); auto. induction H21;contradiction. subst T. Between. spliter. assert_cols. assert(Col A B' B). ColR. assert(A = B' \/ B = B'). apply(l8_9 A B' B); auto. induction H15;contradiction. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel