proposition: Lemma col_cop_orth_at__eq : forall A B C U V X Y, Orth_at X A B C U V -> Coplanar A B C Y -> Col U V Y -> X = Y.
proof: Proof. intros A B C U V X Y HOrth HCop HCol. apply (orth_at2__eq A B C U V); [assumption|]. apply col_cop_orth__orth_at; [exists X|..]; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2