proposition: Lemma perp_in_per_1 : forall A B C D X, Perp_at X A B C D -> Per A X C.
proof: Proof. intros. unfold Perp_at in *. decompose [and] H. apply H5; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR