proposition: Lemma perp_right_comm : forall A B C D, Perp A B C D -> Perp A B D C.
proof: Proof. unfold Perp. intros. ex_and H X. exists X. unfold Perp_at in *. intuition. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR