proposition: Lemma par_cong_mid_os : forall A B A' B', Par_strict A B A' B' -> Cong A B A' B' -> OS A A' B B' -> exists M, Midpoint M A B' /\ Midpoint M B A'.
proof: Proof. intros. assert(HH:= H). unfold Par_strict in HH. spliter. assert(HH:=(midpoint_existence A' B)). ex_and HH X. exists X. prolong A X B'' A X. assert(Midpoint X A B''). unfold Midpoint. split. assumption. Cong. assert(~Col A B A'). intro. apply H3. exists A'. split; Col. assert(Par_strict A B B'' A'). apply (midpoint_par_strict A B B'' A' X). assumption. assumption. apply l7_2. assumption. assert(Col B'' B' A' /\ Col A' B' A'). apply (parallel_uniqueness B A B' A' B'' A' A'). apply par_comm. unfold Par. left. assumption. Col. apply par_left_comm. unfold Par. left. assumption. Col. spliter. assert(Cong A B B'' A'). eapply l7_13. apply l7_2. apply H7. assumption. assert(Cong A' B' A' B''). eapply cong_transitivity. apply cong_symmetry. apply H0. Cong. assert(B' = B'' \/ Midpoint A' B' B''). apply l7_20. Col. Cong. induction H14. subst B''. split. assumption. apply l7_2. assumption. assert(OS A A' X B''). eapply (out_one_side_1 _ _ _ _ A). intro. apply H8. apply col_permutation_1. apply (col_transitivity_1 _ X). intro. subst X. apply is_midpoint_id in H4. subst A'. apply H8. Col. Col. Col. Col. assert_diffs. repeat split; auto. assert(TS A A' B' B''). repeat split. intro. apply H3. exists A. split; Col. unfold OS in H15. ex_and H15 T. unfold TS in H16. spliter. assumption. exists A'. split. Col. unfold Midpoint in H14. spliter. assumption. assert(TS A A' X B'). eapply l9_8_2. apply l9_2. apply H16. apply one_side_symmetry. assumption. assert(OS A A' X B). eapply (out_one_side_1). intro. apply H8. apply col_permutation_1. eapply (col_transitivity_1 _ X). intro. subst X. apply is_midpoint_id in H4. subst A'. apply H3. exists B. split; Col. Col. Col. apply col_trivial_2;Col. assert_diffs. repeat split; Between. assert(OS A A' X B'). eapply one_side_transitivity. apply H18. assumption. apply l9_9 in H17. contradiction. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates