proposition: Lemma chord_completion : forall A B U P, OnCircle U A B -> InCircle P A B -> exists V, OnCircle V A B /\ Bet U P V.
proof: Proof. intros A B U P HOn HIn. destruct (eq_dec_points U A). unfold OnCircle, InCircle in *|-. treat_equalities; exists U; split; Circle; Between. assert (HA' : exists A', U <> A' /\ Col U P A' /\ Per A A' U). { destruct (col_dec U P A) as [HCol|HNCol]. exists A; split; Col; Perp. destruct (l8_18_existence U P A) as [A' [HCol HPerp]]; trivial. assert (U <> A'). { intro; treat_equalities. assert_diffs. destruct (l11_46 P U A) as [_ HLt]; auto. left; Perp. apply lt__nle in HLt. apply HLt. apply (l5_6 A P A B); Cong. } exists A'; repeat split; trivial. apply l8_2, perp_per_1. apply perp_left_comm, perp_col with P; trivial. } destruct HA' as [A' [HUA' [HCol HPer]]]. destruct (symmetric_point_construction U A') as [V HV]. assert_diffs. assert (HCong := per_double_cong A A' U V HPer HV). assert (HVOn : OnCircle V A B). unfold OnCircle in *. apply cong_transitivity with A U; Cong. exists V; split; trivial. apply (col_inc_onc2__bet A B); trivial. ColR. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel