proposition: Lemma perp_in_id : forall A B C X, Perp_at X A B C A -> X = A.
proof: Proof. intros. assert (Perp A B C A). unfold Perp. exists X. assumption. assert (A <> B /\ C <> A). apply perp_distinct. assumption. spliter. assert (HH:=H0). apply perp_perp_in in HH. assert (l8_16_1:=l8_16_1 A B C B A). assert (~Col A B C /\ Per C A B). apply l8_16_1;Col. spliter. unfold Perp_at in H. spliter. apply l8_18_uniqueness with A B C; Col. apply perp_sym. eapply perp_col with A; Col; Perp. intro. subst X. Col. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR