proposition: Lemma eq_o_one_side : forall A B X Y, eq_o A B X A B Y -> OS A B X Y.
proof: Proof. intros. unfold eq_o in H. spliter. assert(A <> B). intro. subst B. apply H. Col. assert(HH:=ex_per_cong B A A X A B). assert(exists P : Tpoint, Per P A B /\ Cong P A A B /\ OS B A P X). apply HH; auto. Col. intro. apply H. Col. clear HH. ex_and H3 T. assert(A <> T). intro. subst T. apply cong_symmetry in H4. apply cong_identity in H4. contradiction. assert(Perp T A A B). apply per_perp_in in H3. apply perp_in_perp_bis in H3. induction H3. apply perp_not_eq_1 in H3. tauto. assumption. auto. assumption. assert(HH:=proj_exists A T X H6). ex_and HH PX. assert(HH:=proj_exists A T Y H6). ex_and HH PY. prolong B A B' B A. prolong PY A C' PY A. assert(Col PX A T). eapply proj_col. apply H8. assert(Col PY A T). eapply proj_col. apply H9. assert(PX <> A). intro. subst PX. apply proj_per in H8. spliter. apply H. apply col_permutation_2. eapply per2__col. apply l8_2. apply H3. assumption. assumption. assumption. assert(PY <> A). intro. subst PY. apply proj_per in H9. spliter. apply H0. apply col_permutation_2. eapply per2__col. apply l8_2. apply H3. assumption. assumption. assumption. assert(~Col T A B). apply per_not_col in H3. assumption. auto. assumption. assert(Col A PX PY). ColR. assert(~Col PX A B). intro. apply H18. ColR. assert(~Col PY A B). intro. apply H18. ColR. assert(A <> C'). intro. subst C'. apply cong_symmetry in H13. apply cong_identity in H13. contradiction. assert(TS A B PY C'). unfold TS. repeat split; auto. intro. apply H21. apply bet_col in H12. ColR. exists A. split. Col. assumption. assert(HH:= H1 PX PY B A B' C' A). assert(Bet PX A C' \/ OS A A PX C'). apply HH; clear HH; clear H1. apply per_perp_in in H3. apply perp_in_comm in H3. apply perp_in_perp_bis in H3. induction H3. apply perp_comm. apply perp_sym. eapply perp_col. auto. apply H1. Col. apply perp_not_eq_1 in H1. tauto. auto. assumption. eapply proj_col_proj. apply H8. auto. Col. apply per_perp_in in H3. apply perp_in_comm in H3. apply perp_in_perp_bis in H3. induction H3. apply perp_comm. apply perp_sym. eapply perp_col. auto. apply H1. Col. apply perp_not_eq_1 in H1. tauto. auto. assumption. eapply proj_col_proj. apply H9. auto. Col. apply out_trivial. auto. apply cong_reflexivity. apply l7_3_2. unfold Midpoint. apply cong_symmetry in H11. split;auto. unfold Midpoint. apply cong_symmetry in H13. split;auto. unfold Midpoint. apply cong_symmetry in H11. split;auto. clear H1 HH. assert(TS A B PX C'). unfold TS. repeat split; auto. intro. apply H21. apply bet_col in H12. ColR. exists A. induction H24. split. Col. assumption. unfold OS in H1. ex_and H1 U. unfold TS in H1. spliter. assert_diffs; tauto. unfold proj in H8. spliter. induction H25. spliter. assert(Par A B X PX). apply l12_9_2D with T A. apply perp_sym. apply H7. apply perp_right_comm. Perp. assert(Par_strict A B X PX). induction H28. assumption. spliter. apply False_ind. apply H. ColR. unfold proj in H9. spliter. induction H30. spliter. assert(Par A B Y PY). apply l12_9_2D with T A. apply perp_sym. apply H7. apply perp_right_comm. Perp. assert(Par_strict A B Y PY). induction H33. assumption. spliter. apply False_ind. apply H0. ColR. apply l12_6 in H29. apply l12_6 in H34. assert(TS A B X C'). eapply l9_8_2. apply H1. apply one_side_symmetry. assumption. assert(TS A B Y C'). eapply l9_8_2. apply H23. apply one_side_symmetry. assumption. eapply l9_8_1. apply H35. assumption. spliter. subst Y. apply l12_6 in H29. eapply one_side_transitivity. apply H29. eapply l9_8_1. apply H1. assumption. spliter. subst X. unfold proj in H9. spliter. induction H26. spliter. assert(Par A B Y PY). apply l12_9_2D with T A. apply perp_sym. apply H7. apply perp_right_comm. Perp. assert(Par_strict A B Y PY). induction H29. assumption. spliter. apply False_ind. apply H0. ColR. apply l12_6 in H30. eapply one_side_transitivity. eapply l9_8_1. apply H1. apply H23. apply one_side_symmetry. assumption. spliter. subst Y. eapply l9_8_1. apply H1. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec