proposition: Lemma l8_9 : forall A B C, Per A B C -> Col A B C -> A=B \/ C=B.
proof: Proof. intros. elim (eq_dec_points A B);intro. tauto. right. eapply l8_7. eapply l8_2. eapply l8_5. apply l8_3 with A; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR