proposition: Lemma chord_lt_diam : forall O P A B U V, ~ Col O U V -> Diam A B O P -> OnCircle U O P -> OnCircle V O P -> Lt U V A B.
proof: Proof. intros. assert(HH:= chord_le_diam O P A B U V H0 H1 H2). unfold Lt. split; auto. intro. apply H. unfold Diam in *. assert(HP:=midpoint_existence U V). ex_and HP O'. unfold Midpoint in *. spliter. unfold OnCircle in *. assert(Cong O A O B) by (apply cong_transitivity with O P; Cong). assert(Cong A O U O'). apply(cong_cong_half_1 A O B U O' V); unfold Midpoint; try split; Cong. assert(Cong B O V O'). apply(cong_cong_half_2 A O B U O' V); unfold Midpoint; try split; Cong. apply(l4_13 O A B). Col. unfold Cong_3. repeat split; Cong; apply cong_transitivity with O P; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel