proposition: Lemma col_cong_mid1 : forall A B C D, A <> D -> Col A B C -> Col A B D -> Cong A B C D -> Cong A C B D -> exists M, Midpoint M A D /\ Midpoint M B C.
proof: Proof. intros. assert(exists M : Tpoint, Midpoint M A C /\ Midpoint M B D \/ Midpoint M A D /\ Midpoint M B C). induction(eq_dec_points A B). subst B. apply cong_symmetry in H2. apply cong_identity in H2. subst D. assert(HH:=midpoint_existence A C). ex_and HH M. exists M. left. tauto. assert (C <> D). intro. subst D. apply cong_identity in H2. contradiction. apply (col_cong_mid A B C D). right. repeat split; ColR. intro. unfold Par_strict in H6. spliter. apply H7. exists C. split; Col. assumption. ex_and H4 M. induction H5. assert(A = B /\ C = D \/ A = D /\ C = B). apply (midpoint_cong_uniqueness A C B D M). Col. assumption. assumption. induction H5. spliter. subst B. subst D. exists M. tauto. spliter. contradiction. exists M. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel