proposition: Lemma bet_onc_le_a : forall O P A B T X, Diam A B O P -> Bet B O T -> OnCircle X O P -> Le T A T X.
proof: Proof. intros. unfold Diam in*. spliter. unfold OnCircle in *. assert(Cong O X O A) by (apply cong_transitivity with O P; Cong). induction(eq_dec_points P O). treat_equalities. apply le_reflexivity. induction(eq_dec_points T O). subst T. apply cong__le;Cong. assert_diffs. apply(triangle_reverse_inequality O T X A); Cong. assert_diffs. repeat split; auto. apply (l5_2 B); Between. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel