proposition: Lemma col_image_spec__eq : forall A B P P', Col A B P -> ReflectL P P' A B -> P = P'.
proof: Proof. intros. apply (l10_6_uniqueness_spec A B P). apply col__image_spec; assumption. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch09_plane GeoCoq.Tarski_dev.Tactics.CoincR_for_cop