proposition: Lemma center_col__diam : forall O P A B, A <> B -> Col O A B -> OnCircle A O P -> OnCircle B O P -> Diam A B O P.
proof: Proof. Proof. intros. unfold Diam. split; Circle. assert(Cong O A O B) by (apply cong_transitivity with O P; Cong). assert(A = B \/ Midpoint O A B) by (apply(l7_20 O A B); Col). induction H4. contradiction. Between. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel