proposition: Lemma cop_onc2__oreq : forall A B C D P Q, InterCCAt A B C D P Q -> Coplanar A C P Q -> forall Z, OnCircle Z A B -> OnCircle Z C D -> Coplanar A C P Z -> Z=P \/ Z=Q.
proof: Proof. intros. assert(HIC := H). unfold InterCCAt in H. spliter. induction (eq_dec_points Z Q). right; auto. left. assert(HH:=midpoint_existence Q P). ex_and HH M. assert(Per A M Q). apply(mid_onc2__per A B Q P M); auto. assert(Per C M Q). apply(mid_onc2__per C D Q P M); auto. assert(HH:=midpoint_existence Z Q). ex_and HH N. assert(Per A N Q). apply(mid_onc2__per A Z Q Z). apply cong_transitivity with A B; Cong. Circle. Midpoint. assert(Per C N Q). apply(mid_onc2__per C Z Q Z). apply cong_transitivity with C D; Cong. Circle. Midpoint. assert(Col A C M). apply cop_per2__col with Q; auto. induction(col_dec P Q A). exists M. left. split; ColR. apply coplanar_perm_12, col_cop__cop with P; Col; Cop. assert_diffs;auto. assert(A <> C). apply(interccat__neq A B C D P Q); auto. assert(Col A C N). apply cop_per2__col with Q; auto. apply coplanar_perm_12, col_cop__cop with Z; Col. apply coplanar_trans_1 with P; Cop. apply interccat__ncol in HIC. Col. assert_diffs;auto. assert(Perp A C Q P). induction(eq_dec_points A M). subst M. apply per_perp_in in H12; auto. apply perp_in_comm in H12. apply perp_in_perp in H12. apply perp_sym. apply (perp_col Q A A C P); Perp. ColR. assert_diffs;auto. apply per_perp_in in H11; auto. apply perp_in_comm in H11. apply perp_in_perp in H11. apply perp_comm in H11. apply (perp_col A M M Q C) in H11; Col. apply perp_sym in H11. apply perp_comm in H11. apply (perp_col Q M C A P) in H11; Col. Perp. assert_diffs;auto. assert(Col Q N Z). ColR. assert(Perp A C Q Z). induction(eq_dec_points A N). subst N. apply per_perp_in in H15; auto. apply perp_in_comm in H15. apply perp_in_perp in H15. apply perp_sym. apply (perp_col Q A A C Z); Perp. assert_diffs;auto. apply per_perp_in in H14; auto. apply perp_in_comm in H14. apply perp_in_perp in H14. apply perp_comm in H14. apply (perp_col A N N Q C) in H14; Col. apply perp_sym in H14. apply perp_comm in H14. apply (perp_col Q N C A Z) in H14; Col. Perp. assert_diffs;auto. apply perp_sym in H21. apply perp_sym in H19. assert (HH : Par Q P Q Z). apply (l12_9 _ _ _ _ A C); auto. Cop. apply coplanar_trans_1 with P; Cop. apply interccat__ncol in HIC. Col. induction HH. unfold Par_strict in H22. spliter. apply False_ind. apply H23. exists Q. split; ColR. spliter. assert(Z = P \/ Z = Q). apply(line_circle_two_points A B P Q Z H4); auto. induction H26; tauto. Qed.
imports: GeoCoq.Tarski_dev.Annexes.circles GeoCoq.Axioms.continuity_axioms