proposition: Lemma incs_onc_diam__lt : forall O P A B U V, Diam A B O P -> InCircleS U O P -> OnCircle V O P -> Lt U V A B.
proof: Proof. intros. unfold Diam in *. spliter. unfold OnCircle in *. unfold InCircleS in *. assert(HH:=segment_construction V O O U). ex_and HH U'. assert(Lt V U' A B). { apply(bet2_lt_le__lt O O A B V U' H4 H). apply cong_transitivity with O P; Cong. apply(cong2_lt__lt O U O P); Cong. } assert(Le V U V U'). { apply(triangle_inequality V O U U' H4); Cong. } apply lt_left_comm. apply(le1234_lt__lt V U V U'); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel