proposition: Lemma ray_cut_chord : forall O P A B X Y, Diam A B O P -> OnCircle X O P -> OnCircle Y O P -> TS A B X Y -> OS X Y O A -> TS X Y O B.
proof: Proof. intros. unfold Diam in *. spliter. apply(l9_8_2 X Y A O B); [|Side]. apply (chord_intersection O P); assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel