proposition: Lemma col_onc2__mid : forall A B U V, U <> V -> OnCircle U A B -> OnCircle V A B -> Col U V A -> Midpoint A U V.
proof: Proof. intros A B U V HUV HU HV HCol. split. apply (col_inc_onc2__bet A B); Circle. apply cong_transitivity with A B; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel