proposition: Lemma chord_par_diam : forall O P A B C C' A' U, O <> P -> ~Col A B C' -> Diam C C' O P -> Midpoint A' A C' -> OnCircle A O P -> OnCircle B O P -> Col A B U -> Perp O U A B -> Par A C' O U -> B = C.
proof: Proof. intros. suma.assert_diffs. assert(Midpoint U A B). { apply(col_onc2_perp__mid O P A B U); Col. } assert(O <> A'). intro. treat_equalities. induction H7. apply H7. exists O. split; Col. spliter. assert(Perp A U O U). { apply perp_sym in H6. apply (perp_col A B O U U); Col. intro. treat_equalities. apply perp_distinct in H6. tauto. } apply perp_left_comm in H18. apply perp_not_col in H18. apply H18; Col. unfold Diam in H1. spliter. assert(HH:=mid_onc2__perp O P A C' A' H15 H13 H3 H17 H2). assert(Perp O U O A'). { apply(par_perp__perp A C' O U O A' H7); Perp. } assert(Par O A' A B). { apply (l12_9_2D _ _ _ _ O U); Perp. } assert(HM:=midpoint_existence B C'). ex_and HM O'. assert(HP:= triangle_mid_par A B C' O' A' H0 H20 H2). apply par_strict_par in HP. assert(Par O A' A' O'). { apply (par_trans _ _ A B); Par. } assert(Col O O' A'). { induction H21. apply False_ind. apply H21. exists A'. split; Col. spliter. Col. } induction(eq_dec_points O O'). treat_equalities. apply(symmetric_point_uniqueness C' O); Midpoint. split; [Between|CongR]. assert(HQ:= mid_onc2__perp O P B C' O' H23 H10 H4 H17 H20). apply(perp_col O A' A C' O') in HH; Col. assert(Par A C' B C'). { apply(l12_9_2D A C' B C' O O'); Perp. } apply False_ind. induction H24. apply H24. exists C'. split;Col. spliter. apply H0. Col. Qed.
imports: GeoCoq.Tarski_dev.Annexes.circles GeoCoq.Tarski_dev.Annexes.half_angles GeoCoq.Tarski_dev.Ch12_parallel_inter_dec