proposition: Lemma onc_col_diam__eq : forall O P A B X, Diam A B O P -> OnCircle X O P -> Col A B X -> X = A \/ X = B.
proof: Proof. intros. unfold Diam in *. spliter. unfold OnCircle in *. induction(eq_dec_points O P). treat_equalities. left; auto. induction(eq_dec_points X B). right; auto. left. assert_diffs. assert(Cong O A O X) by (apply cong_transitivity with O P; Cong). assert(Col A O X) by ColR. assert(HH:= l7_20 O A X H11 H10). induction HH. auto. assert(Midpoint O A B). unfold Midpoint; split; trivial. apply cong_transitivity with O P; Cong. apply False_ind. apply H5. apply (symmetric_point_uniqueness A O ); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel