proposition: Lemma circle_circle_bis__one_point_line_circle : circle_circle_bis -> one_point_line_circle.
proof: Proof. unfold circle_circle_bis, one_point_line_circle. intro Hcc. assert (Haux : forall A B U V P, Col U V P -> U <> V -> Bet A P B -> ~ Per A U V -> exists Z : Tpoint, Col U V Z /\ OnCircle Z A B). { intros A B U V P HCol HUV HBet HNPer. destruct (col_dec U V B) as [|HNCol]. exists B; split; Circle. destruct (eq_dec_points A P). subst P. destruct (diff_col_ex3 U V A) as [W [HUW [HVW [HPW HCol2]]]]; trivial. destruct (segment_construction W A A B) as [Z [HZ1 HZ2]]. exists Z; split; trivial; ColR. destruct (l10_6_existence U V A) as [C HC]. destruct (l10_6_existence U V B) as [D HD]. assert (HBet' : Bet C P D). apply image_gen_preserves_bet with A P B U V; trivial. left; split; trivial. apply col__image_spec, HCol. assert (HCong : Cong B P D P) by (apply (is_image_col_cong U V); assumption). assert (HDIn : InCircle D A B). apply triangle_inequality with P; Cong. assert (HBIn : InCircle B C D). apply triangle_inequality with P; Cong. destruct (Hcc A B C D D B) as [Z0 []]; Circle. destruct (circle_circle_cop A B C D Z0 U) as [Z [HZ1 [HZ2 HCop]]]; trivial. clear dependent Z0. exists Z; split; trivial. apply cong_cop_image__col with A C; trivial. - intro; treat_equalities. assert (Col A U V) by (apply l10_8, HC). apply HNCol; ColR. - apply cong_transitivity with A B; trivial. apply cong_transitivity with C D; Cong. apply cong_symmetry, l10_10 with U V; assumption. - apply coplanar_perm_2. apply coplanar_trans_1 with C; Cop. intro. destruct (eq_dec_points A C). subst C. assert (Col A U V) by (apply l10_8, HC). apply HNCol; ColR. assert (Habs : ReflectL_at U A C U V). apply image_image_in; Col. apply is_image_is_image_spec; auto. destruct Habs as [_ [|]]; auto. apply HNPer. destruct (eq_dec_points A U). subst; Perp. apply perp_per_2, perp_left_comm, perp_col with C; Perp; Col. } intros A B U V P HCol HUV HBet. destruct (per_dec A U V); [|apply Haux with P; assumption]. destruct (Haux A B V U P) as [Z []]; Col. intro; apply HUV, l8_7 with A; assumption. exists Z; split; Col. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Tarski_dev.Annexes.circles GeoCoq.Tarski_dev.Annexes.sums GeoCoq.Utils.all_equiv