proposition: Lemma per13_preserves_bet_inv : forall A B C A' C', Bet A' B C' -> B <> A' -> B <> C' -> Col A B C -> Per B A' A -> Per B C' C -> Bet A B C.
proof: Proof. intros. assert(Col A' B C'). apply bet_col in H. Col. induction(eq_dec_points A A'). subst A'. assert(Col B C' C). ColR. assert(HH:=l8_9 B C' C H4 H6 ). induction HH. contradiction. subst C'. assumption. assert(C <> C'). intro. subst C'. assert(Col B A' A). ColR. assert(HH:=l8_9 B A' A H3 H7). induction HH; contradiction. assert(Perp B A' A' A). 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 B 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 A A' C C'). apply(l12_9 A A' C C' B A'); Perp; Cop. apply perp_sym. apply(perp_col _ C'); Perp. ColR. induction H10. assert(HH:=par_strict_symmetry A A' C C' H10). apply l12_6 in H10. apply l12_6 in HH. assert(~Col A' A B). apply per_not_col in H3; auto. intro. apply H3. Col. assert(~Col C' C B). apply per_not_col in H4; auto. intro. apply H4. Col. assert(OS A' A B C'). apply out_one_side. left; auto. repeat split. intro. subst A'. apply H11. Col. intro. subst C'. apply one_side_symmetry in H10. unfold OS in H10. ex_and H10 X. unfold TS in H10. spliter. apply H10. Col. left. assumption. assert(OS C' C B A'). apply out_one_side. left; auto. repeat split. intro. subst C'. apply H12. Col. intro. subst C'. apply one_side_symmetry in H10. unfold OS in H10. ex_and H10 X. unfold TS in H10. spliter. apply H10. Col. left. Between. assert(OS A' A B C). apply(one_side_transitivity _ _ _ C'); auto. apply invert_one_side. apply one_side_symmetry. assumption. assert(OS C C' B A). apply(one_side_transitivity _ _ _ A'); auto. apply invert_one_side. assumption. apply one_side_symmetry. assumption. apply invert_one_side in H15. assert(HP:= col_one_side_out A A' B C H2 H15). assert(Out C B A). apply(col_one_side_out C C' B A); Col. unfold Out in *. spliter. induction H19. Between. induction H22. Between. apply False_ind. apply H18. apply (between_equality _ _ B); Between. spliter. assert(Perp A' C' A A'). apply (perp_col _ B); Perp. intro. subst C'. apply between_identity in H. subst A'. apply perp_distinct in H9. tauto. apply perp_not_col in H14. apply False_ind. apply H14. ColR. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel