proposition: Lemma perp_in_comm : forall A B C D X, Perp_at X A B C D -> Perp_at X B A D C.
proof: Proof. intros. apply perp_in_left_comm. apply perp_in_right_comm. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR