proposition: Lemma chord_intersection : forall O P A B X Y, OnCircle A O P -> OnCircle B O P -> OnCircle X O P -> OnCircle Y O P -> TS A B X Y -> TS X Y A B.
proof: Proof. intros. unfold TS in H3. spliter. ex_and H5 T. repeat split. apply (onc3__ncol O P); Circle; try(intro; treat_equalities; Col). apply (onc3__ncol O P); Circle; try(intro; treat_equalities; Col). exists T. split. Col. assert_diffs. apply (col_inc_onc2__bet O P); Col. apply(bet_inc2__incs O P X Y T); Circle; intro; treat_equalities; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel