proposition: Lemma l10_8 : forall A B P, Reflect P P A B -> Col P A B.
proof: Proof. intros. induction (eq_dec_points A B). subst;Col. unfold Reflect in H. unfold ReflectL in H. induction H. spliter. ex_and H1 X. apply l7_3 in H1. subst X. Col. spliter. subst. Col. Qed.
imports: GeoCoq.Tarski_dev.Ch09_plane GeoCoq.Tarski_dev.Tactics.CoincR_for_cop