proposition: Lemma col2_orth__orth : forall A B C P Q U V, U <> V -> Col P Q U -> Col P Q V -> Orth A B C P Q -> Orth A B C U V.
proof: Proof. intros A B C P Q U V HUV HU HV [X HX]. exists X. apply col2_orth_at__orth_at with P Q; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2