proposition: Lemma chord_le_diam : forall O P A B U V, Diam A B O P -> OnCircle U O P -> OnCircle V O P -> Le U V A B.
proof: Proof. intros. unfold OnCircle in *. unfold Diam in *. spliter. apply(triangle_inequality_2 U O V A O B); trivial; apply cong_transitivity with O P; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel