proposition: Lemma inc2_le_diam: forall O P A B U V, Diam A B O P -> InCircle U O P -> InCircle V O P -> Le U V A B.
proof: Proof. intros. unfold InCircle in *. unfold Diam in *. spliter. unfold OnCircle in *. assert(HH:= segment_construction U O O V). ex_and HH W. assert(Le U V U W). { apply (triangle_inequality U O); Between; Cong. } assert(Le U W A B). { apply(bet2_le2__le O O A B U W); Between. apply (l5_6 O U O P O U O A);Cong. apply (l5_6 O V O P O W O B);Cong. } apply(le_transitivity U V U W A B); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel