proposition: Lemma perp_perp_in : forall A B C, Perp A B C A -> Perp_at A A B C A.
proof: Proof. intros. apply l8_15_1. unfold Perp in H. ex_and H X. unfold Perp_at in H0. intuition. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR