proposition: Lemma perp_vector : forall A B, A <> B -> (exists X, exists Y, Perp A B X Y).
proof: Proof. intros. exists A. destruct (perp_exists A A B) as [Y]; auto. exists Y; Perp. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR