proposition: Lemma onc4_cong2__eq: forall A B C D O P X, A<>B -> C<>D -> ~ Par A B C D -> OnCircle A O P -> OnCircle B O P -> OnCircle C O P -> OnCircle D O P -> Cong A X B X -> Cong C X D X -> O=X.
proof: Proof. intros. assert(HP:O <> P). { intro. unfold OnCircle in *. treat_equalities. intuition. } assert(HH:= midpoint_existence A B). ex_and HH M. assert(HH:= midpoint_existence C D). ex_and HH N. assert(Col O X M) by (apply(onc2_mid_cong_col O P A B M X); auto). assert(Col O X N) by (apply(onc2_mid_cong_col O P C D N X); auto). induction(eq_dec_points O X). - auto. - assert(Col O M N) by eCol. assert(HH1:=cong_perp_or_mid A B M X H H8 H6). assert(HH2:=cong_perp_or_mid C D N X H0 H9 H7). induction HH1. subst X. induction HH2. subst N. induction(col_dec O A B). assert(A = B \/ Midpoint O A B). unfold OnCircle in *. apply l7_20; Col. apply cong_transitivity with O P; Cong. induction H15. contradiction. assert(M = O). apply (l7_17 A B); auto. subst M; tauto. induction(col_dec O C D). assert(C = D \/ Midpoint O C D). unfold OnCircle in *. apply l7_20; Col. apply cong_transitivity with O P; Cong. induction H16. contradiction. apply (l7_17 C D); auto. assert(HM1:=mid_onc2__perp O P A B M H12 H H2 H3 H8). assert(HM2:=mid_onc2__perp O P C D M H12 H0 H4 H5 H9). apply False_ind. apply H1. apply (l12_9_2D _ _ _ _ O M); Perp. spliter. apply perp_in_perp in H15. induction(col_dec O A B). assert(A = B \/ Midpoint O A B). unfold OnCircle in *. apply l7_20; Col. apply cong_transitivity with O P; Cong. induction H17. contradiction. assert(M = O). apply (l7_17 A B); auto. subst M; tauto. assert(HM1:=mid_onc2__perp O P A B M H12 H H2 H3 H8). apply(perp_col M N C D O ) in H15; Col. apply False_ind. apply H1. apply (l12_9_2D _ _ _ _ O M); Perp. induction HH2. subst X. spliter. induction(col_dec O C D). assert(C = D \/ Midpoint O C D). unfold OnCircle in *. apply l7_20; Col. apply cong_transitivity with O P; Cong. induction H17. contradiction. apply (l7_17 C D); auto. assert(HM1:=mid_onc2__perp O P C D N H12 H0 H4 H5 H9). apply perp_in_perp in H15. apply False_ind. apply H1. apply(perp_col N M A B O) in H15; Col. apply (l12_9_2D _ _ _ _ O N); Perp. spliter. apply perp_in_perp in H17. apply perp_in_perp in H16. apply(perp_col X M A B O) in H17; Col. apply(perp_col X N C D O) in H16; Col. apply False_ind. apply H1. apply (l12_9_2D _ _ _ _ O X); Perp. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel