proposition: Lemma not_par_inter_uniqueness : forall A B C D X Y, A <> B -> C <> D -> ~Par A B C D -> Col A B X -> Col C D X -> Col A B Y -> Col C D Y -> X = Y.
proof: Proof. intros. induction(eq_dec_points C Y). subst Y. induction (eq_dec_points C X). subst X. reflexivity. apply (l6_21 C D A B); auto. intro. apply H1. unfold Par. right. repeat split; ColR. apply (l6_21 A B C D); auto. intro. apply H1. unfold Par. right. repeat split; ColR. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles