proposition: Lemma line_circle_two_points : forall O P U V W, U <> V -> Col U V W -> OnCircle U O P -> OnCircle V O P -> OnCircle W O P -> W = U \/ W = V.
proof: Proof. intros O P U V W HUV HCol HUOn HVOn HWOn. destruct (eq_dec_points W U); auto. right. apply between_equality with U; apply col_inc_onc2__bet with O P; Col; Circle. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel