proposition: Lemma col_orth__orth : forall A B C U V W, U <> W -> Col U V W -> Orth A B C U V -> Orth A B C U W.
proof: Proof. intros A B C U V W HUW HCol HOrth. apply col2_orth__orth with U V; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2