proposition: Lemma incs2_lt_diam : forall O P A B U V, Diam A B O P -> InCircleS U O P -> InCircleS V O P -> Lt U V A B.
proof: Proof. intros. unfold Diam in H. spliter. unfold OnCircle in *. unfold InCircleS in *. induction(eq_dec_points O P). treat_equalities. unfold Lt in H0. spliter. apply le_zero in H. treat_equalities. apply False_ind. apply H0; Cong. assert(Lt A O A B /\ Lt B O A B). { assert (Midpoint O A B). split; [assumption|apply cong_transitivity with O P; Cong]. split. apply(mid__lt ); assert_diffs;auto. assert (Lt B O B A) by (assert_diffs; apply mid__lt; Midpoint). auto using lt_right_comm. } spliter. induction(eq_dec_points O U). treat_equalities. spliter. assert(Lt O V O A). { apply(cong2_lt__lt O V O P); Cong. } apply (lt_transitivity O V O A A B); auto. apply lt_left_comm; auto. assert(HH:=segment_construction U O O V). ex_and HH V'. assert(Le U V U V'). { apply(triangle_inequality U O V V' H8); Cong. } assert(Lt U V' A B). { apply(bet2_lt2__lt O O A B U V' H8 H). apply(cong2_lt__lt O U O P O U O A); Cong. apply(cong2_lt__lt O V O P O V' O B); Cong. } apply(le1234_lt__lt U V U V' A B); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel