proposition: Lemma orth_at_dec : forall A B C U V X, Orth_at X A B C U V \/ ~ Orth_at X A B C U V.
proof: Proof. intros A B C U V X. destruct (orth_dec A B C U V) as [|HNOrth]; [|right; intro HX; apply HNOrth; exists X; apply HX]. destruct (cop_dec A B C X); [|unfold Orth_at; right; intro; spliter; auto]. destruct (col_dec U V X) as [HCol|]; [|unfold Orth_at; right; intro; spliter; auto]. left; apply col_cop_orth__orth_at; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2