proposition: Lemma bet_onc_lt_b : forall O P A B T X, Diam A B O P -> T <> O -> X <> A -> Bet A O T -> OnCircle X O P -> Lt T X T A.
proof: Proof. intros. assert(HH:= bet_onc_le_b O P A B T X H H2 H3 ). assert(Lt T X T A \/ Cong T A T X). { induction(cong_dec T A T X). right; auto. left. unfold Lt. split; Cong. } unfold Diam in *. spliter. unfold OnCircle in *. induction H4; auto. apply False_ind. assert(Bet T O A) by eBetween. assert(Bet T O X). { apply(l4_6 T O A T O X); auto. repeat split. apply cong_reflexivity. assumption. apply cong_transitivity with O P; Cong. } apply H1. apply(between_cong_3 T O); trivial. apply cong_transitivity with O P; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel