proposition: Lemma l8_14_2_1b : forall X A B C D Y, Perp_at X A B C D -> Col Y A B -> Col Y C D -> X=Y.
proof: Proof. intros. unfold Perp_at in H. spliter. apply (H5 Y Y) in H1. apply eq_sym, l8_8; assumption. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR