proposition: Lemma orth_at_symmetry : forall A B C U V X, Orth_at X A B C U V -> Orth_at X A B C V U.
proof: Proof. unfold Orth_at. intros A B C U V X HX; spliter. repeat split; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2