proposition: Lemma midpoint_cong_uniqueness : forall A B C D M, Col A B C -> Midpoint M A B /\ Midpoint M C D -> Cong A B C D -> A = C /\ B = D \/ A = D /\ B = C.
proof: Proof. intros. induction (eq_dec_points A B). subst B. spliter. apply l7_3 in H0. subst M. apply cong_symmetry in H1. apply cong_identity in H1. subst D. apply l7_3 in H2. left. split; assumption. induction(eq_dec_points A C). left. split. assumption. subst C. spliter. eapply symmetric_point_uniqueness. apply H0. assumption. right. spliter. assert(HH:=cong_cong_half_1 A M B C M D H0 H4 H1). assert(A = C \/ Midpoint M A C). apply l7_20. unfold Midpoint in *. spliter. apply bet_col in H0. apply bet_col in H4. ColR. Cong. induction H5. contradiction. assert(B = C). eapply symmetric_point_uniqueness. apply H0. assumption. split. subst C. eapply symmetric_point_uniqueness. apply l7_2. apply H0. assumption. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel