proposition: Lemma bet_onc_lt_a : forall O P A B T X, Diam A B O P -> O <> P -> O <> T -> X <> A -> Bet B O T -> OnCircle X O P -> Lt T A T X.
proof: Proof. intros. assert(HH:= bet_onc_le_a O P A B T X H H3 H4). assert(Lt T A T X \/ Cong T A T X). { induction(cong_dec T A T X). right; auto. left. unfold Lt. split; auto. } induction H5; auto. unfold Diam in*. spliter. unfold OnCircle in *. assert_diffs. assert(Bet O A T \/ Bet O T A). apply(l5_2 B O A T); Between. assert (Cong O A O X) by (apply cong_transitivity with O P; Cong). induction H13. assert(Bet O X T). { apply(l4_6 O A T O X T); auto. unfold Cong_3. repeat split; Cong. } apply False_ind. apply H2. apply(between_cong_2 O T); Cong. assert(Bet O T X). { apply(l4_6 O T A O T X); auto. unfold Cong_3. repeat split; Cong. } apply False_ind. apply H2. apply(between_cong_3 O T); Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel