proposition: Lemma orth_at_chara : forall A B C P X, Orth_at X A B C X P <-> ~ Col A B C /\ X <> P /\ Coplanar A B C X /\ (forall D, Coplanar A B C D -> Per D X P).
proof: Proof. intros A B C P X; split. - unfold Orth_at; intro; spliter. repeat split; Col. - intro; spliter. repeat split; Col. intros; apply per_col with P; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2