proposition: Lemma l8_18_uniqueness : forall A B C X Y, ~ Col A B C -> Col A B X -> Perp A B C X -> Col A B Y -> Perp A B C Y -> X=Y.
proof: Proof. intros. show_distinct A B. solve [intuition]. assert (Perp_at X A B C X) by (eapply l8_15_1;assumption). assert (Perp_at Y A B C Y) by (eapply l8_15_1;assumption). unfold Perp_at in *. spliter. apply l8_7 with C;apply l8_2;[apply H14 |apply H10];Col. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR