proposition: Lemma one_side_eq_o : forall A B C D, A <> B -> OS A B C D -> eq_o A B C A B D.
proof: Proof. intros. assert(HH:= H0). unfold OS in HH. ex_and HH P. unfold TS in H2. assert(~ Col D A B). spliter. assumption. spliter. unfold TS in H1. assert(~ Col C A B). spliter. assumption. spliter. clear H7 H8 H4 H5. unfold eq_o. repeat split. intro. apply H6. Col. intro. apply H3. Col. intros. apply l7_3 in H11. subst M. assert(HH:=H13). unfold Midpoint in HH. spliter. assert(Col A C0 C1). eapply perp2__col. apply perp_sym. apply perp_comm. apply H4. apply perp_sym. Perp. assert(C1 <> A). apply perp_not_eq_2 in H7. assumption. assert(C0 <> A). apply perp_not_eq_2 in H4. assumption. left. induction H16. eapply between_exchange3. apply between_symmetry. apply H16. assumption. induction H16. eapply outer_transitivity_between2. apply H16. assumption. assumption. assert(~Col C1 A B). eapply perp_not_col in H7. intro. apply H7. Col. assert(~Col C0 A B). eapply perp_not_col in H4. intro. apply H4. Col. assert(TS A B C1 C0). unfold TS. repeat split; auto. exists A. split; Col. assert(proj B A C1 A). unfold proj. split. auto. left. repeat split. intro. apply H19. Col. apply perp_comm. Perp. Col. assert(proj C A C1 C0). eapply proj_col_proj. apply H5. auto. apply bet_col in H16. Col. assert( HH:=proj_one_side B C A C0 A C1). assert(Col C B A \/ OS B A C C0). apply HH; auto. induction H24. apply False_ind. apply H6. Col. assert( HH1:=proj_one_side B D A C1 A C1). assert(Col D B A \/ OS B A D C1). apply HH1; auto. induction H25. apply False_ind. apply H3. Col. clear HH HH1. assert(OS A B C0 C1). eapply one_side_transitivity. apply one_side_symmetry. apply invert_one_side. apply H24. eapply one_side_transitivity. apply H0. apply invert_one_side. assumption. apply l9_9 in H21. apply one_side_symmetry in H26. contradiction. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec