proposition: Lemma perp_distinct : forall A B C D, Perp A B C D -> A <> B /\ C <> D.
proof: Proof. intros. unfold Perp in H. ex_elim H X. unfold Perp_at in H0. tauto. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR