proposition: Lemma one_side_eqo : forall A B X Y, OS A B X Y -> eqo A B X A B Y.
proof: Proof. intros. unfold eqo. repeat split. eapply one_side_not_col123. apply H. apply one_side_symmetry in H. eapply one_side_not_col123. apply H. intros. apply l7_3 in H6. subst M. induction(eq_dec_points C C1). subst C1. left. apply midpoint_bet. assumption. assert(A <> C). apply perp_not_eq_2 in H0. auto. assert(A <> C1). apply perp_not_eq_2 in H2. auto. assert(A <> C /\ A <> C1 /\ C <> C1). repeat split; auto. assert(Col A C C1). eapply perp2__col. apply perp_comm. apply perp_sym. apply H0. apply perp_comm. Perp. assert(HH:=diff_col_ex3 A C C1 H13). ex_and HH D. assert(Perp A B D C). apply perp_sym. apply perp_left_comm. eapply perp_col. auto. apply perp_sym. apply H0. Col. assert(~Col A B X). unfold OS in H. ex_and H T. unfold TS in H. spliter. intro. apply H. Col. assert(~Col A B Y). unfold OS in H. ex_and H T. unfold TS in H22. spliter. intro. apply H22. Col. assert(OS A B X C). eapply (per_one_side A B D); auto. apply col_permutation_3. apply H17. Col. assumption. eapply per_col; [|apply H1|]. auto. Col. assert(OS A B Y C1). eapply (per_one_side A B D); auto. apply col_permutation_3. apply H17. apply col_permutation_2. eapply (col_transitivity_1 _ A);Col. assumption. eapply per_col; [|apply H3|]. auto. apply col_permutation_2. eapply (col_transitivity_1 _ C); Col. assert(OS A B C C1). eapply one_side_transitivity. apply one_side_symmetry. apply H23. eapply one_side_transitivity. apply H. assumption. assert(A <> B). apply perp_not_eq_1 in H0. assumption. assert(~ Col C1 A B). unfold OS in H24. ex_and H24 T. unfold TS in H27. spliter. assumption. assert(TS A B C1 C'). unfold TS. repeat split; auto. intro. unfold Midpoint in H8. spliter. assert(C'=A). eapply (l6_21 A B C1 A); Col. subst C'. apply cong_identity in H29. subst C1. tauto. exists A. unfold Midpoint in H8. spliter. split; auto. Col. assert(TS A B C C'). eapply l9_8_2. apply H28. apply one_side_symmetry. assumption. assert(Col A C C'). eapply (col_transitivity_1 _ C1). assumption. Col. unfold Midpoint in H8. spliter. apply bet_col in H8. Col. unfold TS in H29. spliter. ex_and H32 AA. assert(AA=A). apply (l6_21 A B C' C); Col. intro. subst C'. apply between_identity in H33. subst AA. apply H31. assumption. subst AA. left. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec