proposition: Lemma inter_uniqueness_not_par : forall A B C D P, ~Col A B C -> Col A B P -> Col C D P -> ~Par A B C D.
proof: Proof. intros. intro. unfold Par in H2. induction H2. unfold Par_strict in H2. spliter. apply H3. exists P. Col5. spliter. apply H. ColR. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles