proposition: Lemma par_cong_mid_ts : forall A B A' B', Par_strict A B A' B' -> Cong A B A' B' -> TS A A' B B' -> exists M, Midpoint M A A' /\ Midpoint M B B'.
proof: Proof. intros. assert(HH:= H1). unfold TS in HH. assert(~ Col B A A'). spliter; assumption. spliter. ex_and H5 M. exists M. assert(HH:= H). unfold Par_strict in HH. spliter. assert(HH:=(midpoint_existence A A')). ex_and HH X. prolong B X B'' B X. assert(Midpoint X B B''). unfold Midpoint. split. assumption. Cong. assert(Par_strict B A B'' A'). apply (midpoint_par_strict B A B'' A' X); auto. 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. unfold Par. left. assumption. Col. spliter. assert(Cong A B A' B''). eapply l7_13. apply l7_2. apply H9. apply l7_2. assumption. assert(Cong A' B' A' B''). eapply cong_transitivity. apply cong_symmetry. apply H0. assumption. assert(B' = B'' \/ Midpoint A' B' B''). apply l7_20. Col. Cong. induction H18. subst B''. assert(X = M). apply (l6_21 A A' B B'); Col. intro. subst B'. apply H8. exists B. split; Col. subst X. split; auto. assert(TS A A' B B''). unfold TS. repeat split; auto. intro. apply H4. apply col_permutation_1. apply (col_transitivity_1 _ B''). assert_diffs. auto. Col. Col. exists X. split. Col. assumption. assert(OS A A' B' B''). eapply l9_8_1. apply l9_2. apply H1. apply l9_2. assumption. assert(TS A A' B' B''). unfold TS. repeat split. intro. apply H4. Col. intro. apply H4. apply col_permutation_1. apply (col_transitivity_1 _ B''). assert_diffs. auto. Col. Col. exists A'. split. Col. Between. apply l9_9 in H21. contradiction. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates