proposition: Lemma bet_onc_le_b : forall O P A B T X, Diam A B O P -> Bet A O T -> OnCircle X O P -> Le T X T A.
proof: Proof. intros. unfold Diam in *. spliter. unfold OnCircle in *. apply(triangle_inequality T O X A). Between. apply cong_transitivity with O P; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel