proposition: Lemma circle_line : circle_circle -> forall A B C K P Q, CI K C P Q -> InCirc B K -> A <> B -> exists X Y, Definitions.Col A B X /\ Definitions.Col A B Y /\ OnCirc X K /\ OnCirc Y K /\ Definitions.BetS X B Y.
proof: Proof. intros. apply circle_circle__circle_circle_bis in H. apply circle_circle_bis__one_point_line_circle in H. apply one_point_line_circle__two_points_line_circle in H. unfold CI in *. destruct K. destruct p. spliter. injection H0. intros;subst. unfold InCirc in *. unfold two_points_line_circle in H. destruct H1 as [D1 [D2 [HBetS [HCongA [HCongB HBetSB]]]]]. destruct (eq_dec_points B C). subst. assert (HColD: Definitions.Col A C C) by (unfold Definitions.Col;Between). assert (HBet: Bet C C D2) by Between. destruct (H C D2 A C C HColD H2 HBet) as [Z1 [Z2 HZ]]. spliter. exists Z1, Z2. assert (C<>D2) by (unfold Definitions.BetS in *;spliter;auto). repeat split;try assumption; try (intro; treat_equalities; auto); unfold OnCirc;CongR. assert (TwoCases:Definitions.BetS D1 B C \/ Definitions.BetS C B D2) by (apply bet_cases;auto). destruct TwoCases. - assert (HColD: Definitions.Col A B B) by (unfold Definitions.Col;Between). assert (HBet:Bet C B D1) by (unfold Definitions.BetS in *;spliter;Between). destruct (H C D1 A B B HColD H2 HBet) as [Z1 [Z2 HZ]]. exists Z1. exists Z2. spliter. assert (B<>D1) by (unfold Definitions.BetS in *;spliter;auto). assert (Z1<>Z2) by auto. assert (Z1<>B). { intro. subst. unfold OnCircle in *. assert (B=D1) by (apply between_cong with C;auto). subst. intuition. } assert_diffs. assert (B<>Z2). { intro. subst. assert (Bet C Z2 D1) by (unfold BetS in *;spliter;auto). unfold OnCircle in *. assert (Z2=D1) by (apply between_cong with C;auto). intuition. } assert (Definitions.BetS Z1 B Z2) by (unfold Definitions.BetS;auto). unfold OnCirc. repeat split; CongR. - assert (HColD: Definitions.Col A B B) by (unfold Definitions.Col;Between). assert (HBet:Bet C B D2) by (unfold Definitions.BetS in *;spliter;auto). destruct (H C D2 A B B HColD H2 HBet) as [Z1 [Z2 HZ]]. exists Z1. exists Z2. spliter. assert (B<>D2) by (unfold Definitions.BetS in *;spliter;auto). assert (Z1<>Z2) by auto. assert (Z1<>B). { intro. subst. unfold OnCircle in *. assert (B=D2) by (apply between_cong with C;auto). subst. intuition. } assert_diffs. assert (B<>Z2). { intro. subst. assert (Bet C Z2 D2) by (unfold BetS in *;spliter;auto). unfold OnCircle in *. assert (Z2=D2) by (apply between_cong with C;auto). intuition. } assert (Definitions.BetS Z1 B Z2) by (unfold Definitions.BetS;auto). unfold OnCirc. repeat split; CongR. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Axioms.euclidean_axioms GeoCoq.Axioms.continuity_axioms GeoCoq.Meta_theory.Continuity.elementary_continuity_props GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates