proposition: Lemma col_orth_at__orth_at : forall A B C U V W X, U <> W -> Col U V W -> Orth_at X A B C U V -> Orth_at X A B C U W.
proof: Proof. intros A B C U V W X HUW HCol HX. apply col2_orth_at__orth_at with U V; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2