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