proposition: Lemma col2_cop2__eq : forall A B C U V P Q, ~ Coplanar A B C U -> U <> V -> Coplanar A B C P -> Coplanar A B C Q -> Col U V P -> Col U V Q -> P = Q.
proof: Proof. intros A B C U V P Q HNCop; intros. destruct (eq_dec_points P Q); [assumption|]. exfalso. apply HNCop, col_cop2__cop with P Q; ColR. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar