proposition: Lemma perp_proj : forall A B C D, Perp A B C D -> ~Col A C D -> exists X, Col A B X /\ Perp A X C D.
proof: Proof. intros. unfold Perp in H. ex_and H X. exists X. split. unfold Perp_at in H1. spliter. apply col_permutation_1. assumption. eapply perp_col. intro. subst X. unfold Perp_at in H1. spliter. apply H0. assumption. apply perp_in_perp in H1. apply H1. unfold Perp_at in H1. spliter. apply col_permutation_1. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR