proposition: Lemma perp_per_1 : forall A B C, Perp A B C A -> Per B A C.
proof: Proof. intros. assert (Perp_at A A B C A). apply perp_perp_in. assumption. unfold Perp_at in H0. spliter. apply H4. Col. Col. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR