proposition: Lemma l8_14_2_2 : forall X A B C D, Perp A B C D -> (forall Y, Col Y A B -> Col Y C D -> X=Y) -> Perp_at X A B C D.
proof: Proof. intros. eapply l8_14_2_1b_bis. assumption. unfold Perp in H. ex_and H Y. unfold Perp_at in H1. spliter. assert (Col Y C D) by assumption. apply (H0 Y H2) in H3. subst Y. assumption. unfold Perp in H. ex_and H Y. unfold Perp_at in H1. spliter. assert (Col Y C D). assumption. apply (H0 Y H2) in H3. subst Y. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR