proposition: Lemma one_point_line_circle__two_points_line_circle : one_point_line_circle <-> two_points_line_circle.
proof: Proof. unfold one_point_line_circle, two_points_line_circle. split. - intros Hoplc A B U V P HCol HUV HBet. destruct (eq_dec_points P B) as [Heq|HPB]. subst P; exists B, B; repeat split; Circle; Between. destruct (Hoplc A B U V P HCol HUV HBet) as [Z1 [HZ1Col HZ1On]]. exists Z1. assert (HPIn : InCircle P A B) by (apply bet__le1213, HBet). destruct (chord_completion A B Z1 P) as [Z2 [HZ2On HPBet]]; trivial. assert (Z1 <> P). intro; treat_equalities; apply HPB, between_cong with A; trivial. assert_diffs. exists Z2; repeat (split; trivial); ColR. - intros Htplc A B U V P HCol HUV HBet. destruct (Htplc A B U V P HCol HUV HBet) as [Z [_ [HZ1 [HZ2 _]]]]. exists Z; auto. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Tarski_dev.Annexes.circles GeoCoq.Tarski_dev.Annexes.sums GeoCoq.Utils.all_equiv