proposition: Lemma orth_at_distincts : forall A B C U V X, Orth_at X A B C U V -> A <> B /\ B <> C /\ A <> C /\ U <> V.
proof: Proof. unfold Orth_at; intros; spliter; assert_diffs. repeat split; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2