proposition: Lemma segment_circle__one_point_line_circle : segment_circle <-> one_point_line_circle.
proof: Proof. unfold segment_circle, one_point_line_circle. split. - intros Hsc A B U V P HCol HUV HBet. destruct (eq_dec_points A B). unfold InCircle, OnCircle in *. treat_equalities. exists A; Cong. assert (HPIn : InCircle P A B) by (apply bet__le1213; assumption). destruct (diff_col_ex3 U V P) as [W [HUW [HVW [HPW HCol2]]]]; trivial. destruct (eq_dec_points A P). { subst P. destruct (segment_construction W A A B) as [Q [HQ1 HQ2]]. destruct (Hsc A B A Q) as [Z [HZ1 HZ2]]; trivial. apply cong__le; Cong. exists Z; split; trivial. ColR. } destruct (segment_construction W P P A) as [Q0 [HQ01 HQ02]]. destruct (segment_construction P Q0 A B) as [Q [HQ1 HQ2]]. destruct (Hsc A B P Q) as [Z [HZ1 HZ2]]; trivial. apply (l5_6 Q Q0 Q A); Cong. apply (triangle_reverse_inequality P); Cong. assert_diffs. apply l6_6, bet_out; auto. exists Z; split; trivial. ColR. - intros Hoplc A B P Q HPIn HQOut. destruct (eq_dec_points A B). unfold InCircle in HPIn; treat_equalities. exists A; split; Between; Circle. destruct (eq_dec_points P Q). subst Q; exists P; split; Between; Circle. destruct (cong_dec A B A Q) as [HCong|HNCong]. exists Q; split; Between; Circle. assert (HB' : exists B', Cong A B A B' /\ Bet A P B'). { destruct (eq_dec_points A P). subst; exists B; split; Cong; Between. destruct (l6_11_existence A A B P) as [B' [HOut HCong]]; auto. exists B'; split; Cong. apply l6_13_1. apply l6_6, HOut. apply (l5_6 A P A B); Cong. } destruct HB' as [B' [HCong HBet]]. destruct (Hoplc A B' P Q P) as [Z1 [HCol1 HZ1]]; Col. assert (HZ1On: OnCircle Z1 A B) by (apply cong_transitivity with A B'; Cong). clear dependent B'. destruct (or_bet_out P Z1 Q) as [HBet|[HOut|HNCol]]; [exists Z1; auto| |exfalso; apply HNCol; Col]. destruct (chord_completion A B Z1 P) as [Z2 [HZ2On HBet]]; trivial. exists Z2; split; trivial. assert_diffs. assert (HBet2 : Bet Z1 Z2 Q). { apply out2__bet. apply l6_7 with P; trivial. apply l6_6, bet_out; auto. apply (col_inc2_outcs__out A B); Circle. ColR. split; trivial. } eBetween. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Tarski_dev.Annexes.circles GeoCoq.Tarski_dev.Annexes.sums GeoCoq.Utils.all_equiv