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