Require Export GeoCoq.Tarski_dev.Annexes.circles.
Require Export GeoCoq.Tarski_dev.Annexes.half_angles.
Require Export GeoCoq.Tarski_dev.Ch12_parallel_inter_dec.

Section Inscribed_angle.

Context `{TE:Tarski_euclidean}.

(** The sum of the angles of a triangle is the flat angle. *)

Lemma trisuma__bet : forall A B C D E F, TriSumA A B C D E F -> Bet D E F.
Proof.
(* Goal: forall (A B C D E F : @Tpoint Tn) (_ : @TriSumA Tn A B C D E F), @Bet Tn D E F *)
  apply alternate_interior__triangle.
(* Goal: @alternate_interior_angles_postulate Tn *)
  unfold alternate_interior_angles_postulate.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @TS Tn A C B D) (_ : @Par Tn A B C D), @CongA Tn B A C D C A *)
  apply l12_21_a.
Qed.

Lemma bet__trisuma : forall A B C D E F, Bet D E F -> A <> B -> B <> C -> A <> C -> D <> E -> E <> F ->
  TriSumA A B C D E F.
Proof.
(* Goal: forall (A B C D E F : @Tpoint Tn) (_ : @Bet Tn D E F) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) B C)) (_ : not (@eq (@Tpoint Tn) A C)) (_ : not (@eq (@Tpoint Tn) D E)) (_ : not (@eq (@Tpoint Tn) E F)), @TriSumA Tn A B C D E F *)
  intros A B C D E F HBet; intros.
(* Goal: @TriSumA Tn A B C D E F *)
  destruct (ex_trisuma A B C) as [P [Q [R HTri]]]; auto.
(* Goal: @TriSumA Tn A B C D E F *)
  apply conga_trisuma__trisuma with P Q R; trivial.
(* Goal: @CongA Tn P Q R D E F *)
  assert (Hd := HTri).
(* Goal: @CongA Tn P Q R D E F *)
  apply trisuma_distincts in Hd; spliter.
(* Goal: @CongA Tn P Q R D E F *)
  apply conga_line; auto.
(* Goal: @Bet Tn P Q R *)
  apply (trisuma__bet A B C); trivial.
Qed.

Lemma right_saccheris : forall A B C D, Saccheri A B C D -> Per A B C.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)), @ex (@Tpoint Tn) (fun CC : @Tpoint Tn => and (@Cong Tn A CC B CC) (and (@Cong Tn A CC C CC) (@Coplanar Tn A B C CC))) *)
  apply postulates_in_euclidean_context; simpl; repeat (try (left; reflexivity); right).
Qed.

Lemma not_obtuse_saccheris : ~ hypothesis_of_obtuse_saccheri_quadrilaterals.
Proof.
(* Goal: not (@hypothesis_of_obtuse_saccheri_quadrilaterals Tn) *)
  apply not_oah; right.
(* Goal: @hypothesis_of_right_saccheri_quadrilaterals Tn *)
  unfold hypothesis_of_right_saccheri_quadrilaterals; apply right_saccheris.
Qed.

Lemma suma123231__sams : forall A B C D E F, SumA A B C B C A D E F -> SAMS D E F C A B.
Proof. exact (t22_20 not_obtuse_saccheris). Qed.

Lemma bet_suma__suma : forall A B C D E F G H I, G <> H -> H <> I ->
  Bet G H I -> SumA A B C B C A D E F -> SumA D E F C A B G H I.
Proof.
(* Goal: forall (A B C D E F G H I : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) G H)) (_ : not (@eq (@Tpoint Tn) H I)) (_ : @Bet Tn G H I) (_ : @SumA Tn A B C B C A D E F), @SumA Tn D E F C A B G H I *)
  intros A B C D E F G H I HGH HHI HBet HSuma.
(* Goal: @SumA Tn D E F C A B G H I *)
  suma.assert_diffs.
(* Goal: @SumA Tn D E F C A B G H I *)
  destruct (bet__trisuma A B C G H I) as [D' [E' [F' []]]]; auto.
(* Goal: @SumA Tn D E F C A B G H I *)
  apply (conga3_suma__suma D' E' F' C A B G H I); try apply conga_refl; auto.
(* Goal: @CongA Tn D' E' F' D E F *)
  apply (suma2__conga A B C B C A); assumption.
Qed.

Lemma high_school_exterior_angle_theorem : forall A B C B', A <> B -> B <> C -> A <> C -> A <> B' ->
  Bet B A B' -> SumA A B C B C A C A B'.
Proof.
(* Goal: forall (A B C B' : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) B C)) (_ : not (@eq (@Tpoint Tn) A C)) (_ : not (@eq (@Tpoint Tn) A B')) (_ : @Bet Tn B A B'), @SumA Tn A B C B C A C A B' *)
  intros A B C B'; intros.
(* Goal: @SumA Tn A B C B C A C A B' *)
  assert (SumA C A B' C A B B A B').
(* Goal: @SumA Tn C A B' C A B B A B' *)
(* Goal: @SumA Tn A B C B C A C A B' *)
    apply suma_sym, suma_left_comm, bet__suma; auto.
(* Goal: @SumA Tn A B C B C A C A B' *)
  destruct (ex_suma A B C B C A) as [D [E [F]]]; auto.
(* Goal: @SumA Tn A B C B C A C A B' *)
  apply (conga3_suma__suma A B C B C A D E F); try apply conga_refl; auto.
(* Goal: @CongA Tn D E F C A B' *)
  apply sams2_suma2__conga123 with C A B B A B'.
(* Goal: @SAMS Tn D E F C A B *)
(* Goal: @SAMS Tn C A B' C A B *)
(* Goal: @SumA Tn D E F C A B B A B' *)
(* Goal: @SumA Tn C A B' C A B B A B' *)
    apply suma123231__sams; assumption.
(* Goal: @SAMS Tn C A B' C A B *)
(* Goal: @SumA Tn D E F C A B B A B' *)
(* Goal: @SumA Tn C A B' C A B B A B' *)
    apply bet_suma__sams with B A B'; assumption.
(* Goal: @SumA Tn D E F C A B B A B' *)
(* Goal: @SumA Tn C A B' C A B B A B' *)
    apply bet_suma__suma; auto.
(* Goal: @SumA Tn C A B' C A B B A B' *)
    assumption.
Qed.

(** If A, B and C are points on a circle where the line AB is a diameter of the circle,
    then the angle ACB is a right angle. *)

Lemma thales_theorem : forall A B C M, ~ Col A B C ->
  Midpoint M A B -> Cong M A M C -> Per A C B.
Proof.
(* Goal: forall (A B C M : @Tpoint Tn) (_ : not (@Col Tn A B C)) (_ : @Midpoint Tn M A B) (_ : @Cong Tn M A M C), @Per Tn A C B *)
  apply rah__thales_postulate.
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
  unfold postulate_of_right_saccheri_quadrilaterals; apply right_saccheris.
Qed.

(** In a right triangle, the midpoint of the hypotenuse is the circumcenter. *)

Lemma thales_converse_theorem : forall A B C M, A <> C -> B <> C ->
  Midpoint M A B -> Per A C B -> Cong M A M C.
Proof.
(* Goal: forall (A B C M : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A C)) (_ : not (@eq (@Tpoint Tn) B C)) (_ : @Midpoint Tn M A B) (_ : @Per Tn A C B), @Cong Tn M A M C *)
  intros A B C M HAC HBC HM HPer.
(* Goal: @SumA Tn C A B' C A B B A B' *)
  apply thales_postulate__thales_converse_postulate with B; [| |assumption..].
(* Goal: @thales_postulate Tn *)
(* Goal: not (@Col Tn A B C) *)
    unfold thales_postulate; apply thales_theorem.
(* Goal: not (@Col Tn A B C) *)
  apply not_col_permutation_5, per_not_col; auto.
Qed.

Lemma bet_cong__ghalfa : forall A B C B', A <> B -> B <> C -> A <> B' ->
  Bet B A B' -> Cong A B A C -> gHalfA A B C C A B'.
Proof.
(* Goal: forall (A B C B' : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) B C)) (_ : not (@eq (@Tpoint Tn) A B')) (_ : @Bet Tn B A B') (_ : @Cong Tn A B A C), @gHalfA Tn A B C C A B' *)
  intros A B C B' HAB HBC HAB' HBet HCong.
(* Goal: @gHalfA Tn A B C C A B' *)
  apply ghalfa_chara; split.
(* Goal: @Acute Tn O C' B *)
    apply cong__acute; auto.
(* Goal: @eq (@Tpoint Tn) O O' *)
  assert_diffs.
(* Goal: @SumA Tn A B C A B C C A B' *)
  apply (conga3_suma__suma A B C B C A C A B'); try apply conga_refl; auto.
(* Goal: @SumA Tn A B C B C A C A B' *)
(* Goal: @CongA Tn B C A A B C *)
    apply high_school_exterior_angle_theorem; auto.
(* Goal: @CongA Tn B C A A B C *)
  apply conga_left_comm, l11_44_1_a; Cong.
Qed.

(** If the angle ACB is inscribed in a circle of center O and
    C, O lie on the same side of AB, then this angle is acute. *)

Lemma onc3_os__acute : forall O P A B C,
  OnCircle A O P -> OnCircle B O P -> OnCircle C O P -> OS A B O C ->
  Acute A C B.
Proof.
(* Goal: forall (O P A B C : @Tpoint Tn) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @OS Tn A B O C), @gHalfA Tn A C B A O B *)
  intros O P A B C HA HB HC HOS.
(* Goal: @eq (@Tpoint Tn) O O' *)
  destruct (midpoint_existence A B) as [M HM].
(* Goal: @Acute Tn A C B *)
  assert (HNCol : ~ Col A B C) by (eapply one_side_not_col124, HOS).
(* Goal: @Acute Tn A C B *)
  assert (HLt : Lt M A M C).
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
  { assert (HNCol1 : ~ Col A B O) by (eapply one_side_not_col123, HOS).
(* Goal: @Lt Tn M A M C *)
    assert (M <> O) by (intro; treat_equalities; apply HNCol1; Col).
(* Goal: @gHalfA Tn A C B A O B *)
    assert (O <> C) by (intro; treat_equalities; auto).
(* Goal: @eq (@Tpoint Tn) O O' *)
    assert_diffs.
(* Goal: @Lt Tn M A M C *)
    assert (Cong O A O C) by (apply (onc2__cong O P); assumption).
(* Goal: @Lt Tn M A M C *)
    destruct (angle_partition M O C); auto.
    - assert (HMO := H).
(* Goal: @Lt Tn M A M C *)
      clear H.
(* Goal: @Lt Tn M A M C *)
      destruct (l8_18_existence M O C) as [H []].
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
      { intro.
(* Goal: False *)
        destruct (acute_col__out M O C) as [_ [_ [HBet|HBet]]]; auto.
        - apply l9_9_bis in HOS.
(* Goal: False *)
          apply HOS.
(* Goal: @TS Tn A B O C *)
          repeat split; Col.
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A B) (@Bet Tn O T C)) *)
          exists M; split; Col.
        - apply (le__nlt O C O M); Le.
(* Goal: @Lt Tn O M O C *)
          apply (cong2_lt__lt O M O P); Cong.
(* Goal: @Lt Tn O M O P *)
          apply bet_inc2__incs with A B; Circle; Between.
      }
(* Goal: @Lt Tn M A M C *)
      assert (Perp O M A B) by (apply mid_onc2__perp with P; auto).
(* Goal: @Lt Tn M A M C *)
      assert (HOS1 : OS A B C H).
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
      { apply l12_6, par_not_col_strict with C; Col.
(* Goal: @Par Tn A B C H *)
        apply l12_9 with O M; Perp; [|Cop| |Cop].
(* Goal: @Coplanar Tn O M A C *)
(* Goal: @Coplanar Tn O M B C *)
          apply coplanar_perm_5, col_cop__cop with B; Col; Cop.
(* Goal: @Coplanar Tn O M B C *)
          apply coplanar_perm_5, col_cop__cop with A; Col; Cop.
      }
(* Goal: @Lt Tn M A M C *)
      assert (M <> H) by (intro; subst; apply one_side_not_col124 in HOS1; apply HOS1; Col).
(* Goal: @Lt Tn M A M C *)
      assert (Per M H C) by (apply perp_per_1, perp_left_comm, perp_col with O; Col).
(* Goal: @Lt Tn M A M C *)
      apply lt_transitivity with H C; [|assert_diffs; apply l11_46; auto].
(* Goal: @Lt Tn M A H C *)
      apply cong_lt_per2__lt_1 with O O; Cong.
(* Goal: @Per Tn O H C *)
(* Goal: @Per Tn O M A *)
(* Goal: @Lt Tn O H O M *)
        apply l8_2, per_col with M; Col; Perp.
(* Goal: @Per Tn O M A *)
(* Goal: @Lt Tn O H O M *)
        apply perp_per_1, perp_left_comm, perp_col1 with B; Col.
(* Goal: @Lt Tn O H O M *)
      apply bet__lt1213; auto; apply out2__bet.
(* Goal: @Out Tn O H M *)
(* Goal: @Out Tn M O H *)
        apply (acute_col_perp__out C); [apply acute_sym|..]; Col; Perp.
(* Goal: @SumA Tn C A B' C A B B A B' *)
        apply (l9_19 A B); Col; apply one_side_transitivity with C; assumption.
    - apply lt_transitivity with O C; [|apply l11_46; auto].
(* Goal: @Lt Tn M A O C *)
      apply (cong2_lt__lt M A O A); Cong.
(* Goal: @Lt Tn M A O A *)
      apply l11_46; auto.
(* Goal: or (@Per Tn O M A) (@Obtuse Tn O M A) *)
      left.
(* Goal: @Per Tn O M A *)
      apply mid_onc2__per with P B; auto.
  }
(* Goal: @Acute Tn A C B *)
  destruct HLt as [[C' [HBet HCong]] HNCong].
(* Goal: @Acute Tn A C B *)
  exists A, C', B; split.
(* Goal: @Per Tn A C' B *)
(* Goal: @LtA Tn A C B A C' B *)
    apply thales_theorem with M; trivial; intro; apply HNCol; ColR.
(* Goal: @eq (@Tpoint Tn) O O' *)
  assert_diffs.
(* Goal: @LtA Tn A C B A C' B *)
  assert (C <> C') by (intro; subst; apply HNCong, HCong).
(* Goal: @LtA Tn A C B A C' B *)
  apply os3__lta.
  - apply one_side_transitivity with M.
(* Goal: @OS Tn C B A M *)
(* Goal: @OS Tn C B M C' *)
      apply invert_one_side, out_one_side; [Col|apply l6_6, bet_out; Between].
(* Goal: @OS Tn C B M C' *)
      apply out_one_side; [left; intro; apply HNCol; ColR|apply l6_6, bet_out; Between].
  - apply out_one_side_1 with M; Col; apply l6_6, bet_out; auto.
  - apply one_side_transitivity with M.
(* Goal: @OS Tn C B A M *)
(* Goal: @OS Tn C B M C' *)
      apply invert_one_side, out_one_side; [Col|apply l6_6, bet_out; Between].
(* Goal: @OS Tn C B M C' *)
      apply out_one_side; [left; intro; apply HNCol; ColR|apply l6_6, bet_out; Between].
Qed.

Lemma inscribed_angle_aux : forall O P A B C,
  OnCircle A O P -> OnCircle B O P -> OnCircle C O P ->
  OS A B O C -> TS O C A B ->
  gHalfA A C B A O B.
Proof.
(* Goal: forall (O P A B C : @Tpoint Tn) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @OS Tn A B O C) (_ : @TS Tn O C A B), @gHalfA Tn A C B A O B *)
  intros O P A B C HA HB HC HOS HTS.
(* Goal: @gHalfA Tn A C B A O B *)
  destruct (segment_construction C O O P) as [C' []].
(* Goal: @eq (@Tpoint Tn) O O' *)
  assert_diffs.
(* Goal: @gHalfA Tn A C B A O B *)
  assert (O <> C') by (intro; treat_equalities; auto).
(* Goal: @eq (@Tpoint Tn) O O' *)
  assert (HCong := (onc2__cong O P)).
(* Goal: @gHalfA Tn A C B A O B *)
  apply suma_preserves_ghalfa with A C C' C' C B A O C' C' O B.
(* Goal: @SumA Tn C A B' C A B B A B' *)
    apply (onc3_os__acute O P); assumption.
(* Goal: @SumA Tn A C C' C' C B A C B *)
(* Goal: @SumA Tn A O C' C' O B A O B *)
(* Goal: @gHalfA Tn A C C' A O C' *)
(* Goal: @gHalfA Tn C' C B C' O B *)
    apply ts__suma, invert_two_sides, col_two_sides with O; Side; Col.
(* Goal: @SumA Tn A O C' C' O B A O B *)
(* Goal: @gHalfA Tn A C C' A O C' *)
(* Goal: @gHalfA Tn C' C B C' O B *)
    apply ts__suma, invert_two_sides, col_two_sides with C; Col.
    apply ghalfa_out4__ghalfa with A O A C'; try apply out_trivial; auto;
      [apply l6_6, bet_out|apply ghalfa_left_comm, bet_cong__ghalfa]; auto.
    apply ghalfa_out4__ghalfa with O B C' B; try apply out_trivial; auto;
      [apply l6_6, bet_out|apply ghalfa_right_comm, bet_cong__ghalfa]; auto.
Qed.

Lemma inscribed_angle_aux1 : forall O P A B C,
  OnCircle A O P -> OnCircle B O P -> OnCircle C O P ->
  OS A B O C -> OS O C A B ->
  gHalfA A C B A O B.
Proof.
  assert (Haux : forall O P A B C, OnCircle A O P -> OnCircle B O P -> OnCircle C O P ->
  OS A B O C -> OS O C A B -> OS O B A C -> gHalfA A C B A O B).
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
  { intros O P A B C HA HB HC HOS1 HOS2 HOS3.
(* Goal: @gHalfA Tn A C B A O B *)
    destruct (chord_completion O P C O) as [C' [HC' HBet ]]; Circle.
(* Goal: @eq (@Tpoint Tn) O O' *)
    assert_diffs.
(* Goal: @gHalfA Tn A C B A O B *)
    assert (C' <> O) by (intro; treat_equalities; auto).
(* Goal: @gHalfA Tn A C B A O B *)
    assert (TS O B A C').
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
    { apply l9_8_2 with C; [|Side].
(* Goal: @TS Tn O B C C' *)
      apply one_side_not_col124 in HOS3.
(* Goal: @TS Tn O B C C' *)
      repeat split.
(* Goal: not (@Col Tn C O B) *)
(* Goal: not (@Col Tn C' O B) *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T O B) (@Bet Tn C T C')) *)
        Col.
(* Goal: not (@Col Tn C' O B) *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T O B) (@Bet Tn C T C')) *)
        intro; apply HOS3; ColR.
(* Goal: not (@Col Tn C O B) *)
(* Goal: not (@Col Tn C' O B) *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T O B) (@Bet Tn C T C')) *)
      exists O; split; Col.
    }
(* Goal: @eq (@Tpoint Tn) O O' *)
    assert (HCong := (onc2__cong O P)).
(* Goal: @gHalfA Tn A C B A O B *)
    apply acute_ghalfa2_sams_suma2__ghalfa123 with B C O A C O B O C' A O C'.
    - repeat split; auto.
(* Goal: not (@Col Tn C O B) *)
(* Goal: not (@Col Tn C' O B) *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T O B) (@Bet Tn C T C')) *)
        right; intro; assert_cols; assert_ncols; Col.
(* Goal: @SumA Tn A O B B O C' A O C' *)
      exists C'.
(* Goal: and (@CongA Tn B O C' B O C') (and (not (@OS Tn O B A C')) (and (not (@TS Tn A O B C')) (@Coplanar Tn A O B C'))) *)
      split; CongA.
(* Goal: and (not (@OS Tn O B A C')) (and (not (@TS Tn A O B C')) (@Coplanar Tn A O B C')) *)
      repeat split; [Side| |Cop].
(* Goal: not (@TS Tn A O B C') *)
      apply l9_9_bis, invert_one_side, one_side_symmetry, os_ts1324__os; [|Side].
(* Goal: @OS Tn O C' B A *)
      apply col_one_side with C; Col; Side.
(* Goal: @SumA Tn C A B' C A B B A B' *)
    - apply (onc3_os__acute O P); assumption.
    - exists O.
(* Goal: and (@CongA Tn B C O B C O) (and (not (@OS Tn C B A O)) (and (@Coplanar Tn A C B O) (@CongA Tn A C O A C O))) *)
      repeat (split; CongA); [|Cop].
(* Goal: not (@OS Tn C B A O) *)
      apply l9_9, invert_two_sides, l9_31; Side.
    - exists C'.
(* Goal: and (@CongA Tn B O C' B O C') (and (not (@OS Tn O B A C')) (and (@Coplanar Tn A O B C') (@CongA Tn A O C' A O C'))) *)
      repeat (split; CongA); [Side|Cop].
    - apply ghalfa_left_comm, bet_cong__ghalfa; auto.
    - apply ghalfa_left_comm, bet_cong__ghalfa; auto.
  }
(* Goal: forall (O P A B C : @Tpoint Tn) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @OS Tn A B O C) (_ : @OS Tn O C A B), @gHalfA Tn A C B A O B *)
  intros O P A B C HA HB HC HOS1 HOS2.
(* Goal: @CongA Tn A C B A C' B *)
  assert_ncols.
(* Goal: @gHalfA Tn A C B A O B *)
  destruct (cop__one_or_two_sides O B A C) as [HTS|]; Col; Cop.
(* Goal: @gHalfA Tn A C B A O B *)
(* Goal: @gHalfA Tn A C B A O B *)
    apply ghalfa_comm, Haux with P; auto; [..|apply one_side_symmetry, os_ts1324__os]; Side.
(* Goal: @SumA Tn C A B' C A B B A B' *)
    apply Haux with P; assumption.
Qed.

(** Euclid Book III Prop 20:
    In a circle the angle at the centre is double of the angle at the circumference,
    when the angles have the same circumference as base. *)

Lemma inscribed_angle : forall O P A B C,
  OnCircle A O P -> OnCircle B O P -> OnCircle C O P -> OS A B O C ->
  gHalfA A C B A O B.
Proof.
(* Goal: forall (O P A B C : @Tpoint Tn) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @OS Tn A B O C), @gHalfA Tn A C B A O B *)
  intros O P A B C HA HB HC HOS.
(* Goal: @eq (@Tpoint Tn) O O' *)
  assert (HCong := (onc2__cong O P)).
(* Goal: @gHalfA Tn A C B A O B *)
  destruct (col_dec A O C).
(* Goal: @eq (@Tpoint Tn) O O' *)
  { assert_diffs.
(* Goal: @gHalfA Tn A C B A O B *)
    assert (Bet C O A) by (apply col_inc_onc2__bet with O P; Col; Circle).
(* Goal: @gHalfA Tn A C B A O B *)
    assert (O <> C) by (intro; treat_equalities; auto).
(* Goal: @gHalfA Tn A C B A O B *)
    apply ghalfa_right_comm, ghalfa_out4__ghalfa with O B B A; try apply out_trivial; auto.
(* Goal: @Out Tn C C' O *)
(* Goal: @Out Tn C B B *)
(* Goal: @Acute Tn O C B *)
      apply l6_6, bet_out; auto.
(* Goal: @gHalfA Tn O C A A O B *)
    apply bet_cong__ghalfa; auto.
  }
(* Goal: @gHalfA Tn A C B A O B *)
  destruct (col_dec B O C).
(* Goal: @eq (@Tpoint Tn) O O' *)
  { assert_diffs.
(* Goal: @gHalfA Tn A C B A O B *)
    assert (Bet C O B) by (apply col_inc_onc2__bet with O P; Col; Circle).
(* Goal: @gHalfA Tn A C B A O B *)
    assert (O <> C) by (intro; treat_equalities; auto).
(* Goal: @gHalfA Tn A C B A O B *)
    apply ghalfa_left_comm, ghalfa_out4__ghalfa with O A A B; try apply out_trivial; auto.
(* Goal: @Out Tn C C' O *)
(* Goal: @Out Tn C B B *)
(* Goal: @Acute Tn O C B *)
      apply l6_6, bet_out; auto.
(* Goal: @gHalfA Tn O C A A O B *)
    apply bet_cong__ghalfa; auto.
  }
(* Goal: @gHalfA Tn A C B A O B *)
  destruct (cop__one_or_two_sides O C A B); Cop.
(* Goal: @SumA Tn C A B' C A B B A B' *)
    apply inscribed_angle_aux with P; assumption.
(* Goal: @SumA Tn C A B' C A B B A B' *)
    apply inscribed_angle_aux1 with P; assumption.
Qed.

Lemma diam_onc2_ts__suppa : forall O P A B C C',
  OnCircle A O P -> OnCircle B O P -> Diam C C' O P -> TS A B C C' ->
  SuppA A C B A C' B.
Proof.
(* Goal: forall (O P A B C C' : @Tpoint Tn) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @Diam Tn C C' O P) (_ : @TS Tn A B C C'), @SuppA Tn A C B A C' B *)
  intros O P A B C C' HA HB [HBet [HC HC']] HTS.
(* Goal: @eq (@Tpoint Tn) O O' *)
  assert_diffs.
(* Goal: @eq (@Tpoint Tn) O O' *)
  assert (HCong := onc2__cong O P).
(* Goal: @SuppA Tn A C B A C' B *)
  assert (HMid : Midpoint O C C') by (split; Cong).
(* Goal: @SuppA Tn A C B A C' B *)
  assert (C <> C') by (intro; treat_equalities; auto).
(* Goal: @SuppA Tn A C B A C' B *)
  assert (HNColA : ~ Col C C' A) by (apply (onc3__ncol O P); auto).
(* Goal: @SuppA Tn A C B A C' B *)
  assert (HNColB : ~ Col C C' B) by (apply (onc3__ncol O P); auto).
(* Goal: @SuppA Tn A C B A C' B *)
  assert (HSumaA : SumA A C C' C C' A C A C') by (apply cong_mid__suma with O; auto).
(* Goal: @SuppA Tn A C B A C' B *)
  assert (HSumaB : SumA B C C' C C' B C B C') by (apply cong_mid__suma with O; auto).
(* Goal: @SuppA Tn A C B A C' B *)
  assert (Per C A C') by (apply thales_theorem with O; auto).
(* Goal: @SuppA Tn A C B A C' B *)
  assert (Per C B C') by (apply thales_theorem with O; auto).
(* Goal: @SuppA Tn A C B A C' B *)
  assert (HSuma : SumA C A C' C B C' C O C') by (assert_diffs; apply bet_per2__suma; auto).
(* Goal: @SuppA Tn A C B A C' B *)
  apply bet_suma__suppa with C O C'; trivial.
(* Goal: @SumA Tn A C B A C' B C O C' *)
  destruct (ex_suma C A C' C' C B) as [D [E [F HSuma1]]]; auto.
(* Goal: @SumA Tn A C B A C' B C O C' *)
  assert (HTS2 : TS C C' A B) by (apply (chord_intersection O P); assumption).
(* Goal: @SumA Tn A C B A C' B C O C' *)
  assert (HTS3 : TS C' C A B) by (apply invert_two_sides, HTS2).
(* Goal: @SumA Tn A C B A C' B C O C' *)
  assert (Acute C' C A).
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
  { assert_diffs; apply acute_out2__acute with O A.
(* Goal: @Out Tn C C' O *)
(* Goal: @Out Tn C B B *)
(* Goal: @Acute Tn O C B *)
      apply l6_6, bet_out; auto.
(* Goal: @Out Tn C' B B *)
(* Goal: @Acute Tn O C' B *)
      apply out_trivial; auto.
(* Goal: @Acute Tn O C' B *)
      apply cong__acute; auto.
  }
(* Goal: @SumA Tn A C B A C' B C O C' *)
  assert (Acute C' C B).
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
  { assert_diffs; apply acute_out2__acute with O B.
(* Goal: @Out Tn C C' O *)
(* Goal: @Out Tn C B B *)
(* Goal: @Acute Tn O C B *)
      apply l6_6, bet_out; auto.
(* Goal: @Out Tn C' B B *)
(* Goal: @Acute Tn O C' B *)
      apply out_trivial; auto.
(* Goal: @Acute Tn O C' B *)
      apply cong__acute; auto.
  }
(* Goal: @SumA Tn A C B A C' B C O C' *)
  assert (Acute C C' A).
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
  { assert_diffs; apply acute_out2__acute with O A.
(* Goal: @Out Tn C' C O *)
(* Goal: @Out Tn C' B B *)
(* Goal: @Acute Tn O C' B *)
      apply l6_6, bet_out; Between.
(* Goal: @Out Tn C' B B *)
(* Goal: @Acute Tn O C' B *)
      apply out_trivial; auto.
(* Goal: @Acute Tn O C' B *)
      apply cong__acute; auto.
  }
(* Goal: @SumA Tn A C B A C' B C O C' *)
  assert (Acute C C' B).
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
  { assert_diffs; apply acute_out2__acute with O B.
(* Goal: @Out Tn C' C O *)
(* Goal: @Out Tn C' B B *)
(* Goal: @Acute Tn O C' B *)
      apply l6_6, bet_out; Between.
(* Goal: @Out Tn C' B B *)
(* Goal: @Acute Tn O C' B *)
      apply out_trivial; auto.
(* Goal: @Acute Tn O C' B *)
      apply cong__acute; auto.
  }
(* Goal: @SumA Tn A C B A C' B C O C' *)
  assert (HSuma2 : SumA A C B A C' C D E F).
(* Goal: @SumA Tn A C B A C' C D E F *)
(* Goal: @SumA Tn A C B A C' B C O C' *)
    apply suma_sym, suma_assoc_1 with A C C' C' C B C A C'; SumA.
(* Goal: @SumA Tn A C B A C' B C O C' *)
  assert (HSAMS : SAMS A C B A C' C).
(* Goal: @SAMS Tn A C B A C' C *)
(* Goal: @SumA Tn A C B A C' B C O C' *)
    apply sams_sym, sams_assoc_1 with A C C' C' C B C A C'; SumA.
(* Goal: @SumA Tn A C B A C' B C O C' *)
  apply suma_assoc_1 with A C' C C C' B D E F; [SumA..|].
(* Goal: @SumA Tn D E F C C' B C O C' *)
  apply suma_assoc_2 with C A C' B C C' C B C'; SumA.
Qed.

(** In a circle the angle at the centre is double of the angle at the circumference. *)

Lemma inscribed_angle_1 : forall O P A B C, A <> B -> B <> C -> A <> C ->
  OnCircle A O P -> OnCircle B O P -> OnCircle C O P -> Coplanar A B C O ->
  SumA A C B A C B A O B.
Proof.
(* Goal: forall (O P A B C : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) B C)) (_ : not (@eq (@Tpoint Tn) A C)) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @Coplanar Tn A B C O), @SumA Tn A C B A C B A O B *)
  intros O P A B C HAB HBC HAC HA HB HC HCop.
(* Goal: @TS Tn A B O C *)
  assert (~ Col A B C) by (apply (onc3__ncol O P); auto).
(* Goal: @SuppA Tn A C B A C' B *)
  destruct (col_dec A B O).
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
  { assert (Midpoint O A B) by (apply col_onc2__mid with P; auto).
(* Goal: @SumA Tn A C B A C B A O B *)
    assert (Per A C B) by (apply thales_theorem with O; auto; apply cong_transitivity with O P; Cong).
(* Goal: @SumA Tn A C B A C B A O B *)
    assert_diffs; apply bet_per2__suma; Between.
  }
(* Goal: @SuppA Tn A C B A C' B *)
  destruct (cop__one_or_two_sides A B O C); Col; Cop.
  - destruct (chord_completion O P C O) as [C' []]; Circle.
(* Goal: @SumA Tn A C B A C B A O B *)
    assert (TS A B C' C) by (apply l9_2, bet_ts__ts with O; Side).
(* Goal: @SumA Tn A C B A C B A O B *)
    assert (SuppA A C' B A C B).
(* Goal: @SuppA Tn A C' B A C B *)
(* Goal: @SumA Tn A C B A C B A O B *)
      apply (diam_onc2_ts__suppa O P); [..|repeat split|]; Between.
(* Goal: @SumA Tn A C B A C B A O B *)
    apply (suma_suppa2__suma A C' B A C' B); trivial.
(* Goal: @SumA Tn A C B A C B A O B *)
    apply ghalfa__suma, inscribed_angle with P; trivial.
(* Goal: @OS Tn A B O C' *)
    exists C; split; trivial.
  - apply ghalfa__suma, inscribed_angle with P; trivial.
Qed.

(** If two angles ACB and ADB are inscribed in the same circle,
    then they are either congruent or supplementary. *)

Lemma cop2_onc4__or_conga_suppa : forall O P A B C C',
  A <> B -> B <> C -> A <> C -> B <> C' -> A <> C' ->
  OnCircle A O P -> OnCircle B O P -> OnCircle C O P -> OnCircle C' O P ->
  Coplanar A B C O -> Coplanar A B C' O ->
  CongA A C B A C' B \/ SuppA A C B A C' B.
Proof.
(* Goal: forall (O P A B C C' : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) B C)) (_ : not (@eq (@Tpoint Tn) A C)) (_ : not (@eq (@Tpoint Tn) B C')) (_ : not (@eq (@Tpoint Tn) A C')) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @OnCircle Tn C' O P) (_ : @Coplanar Tn A B C O) (_ : @Coplanar Tn A B C' O), or (@CongA Tn A C B A C' B) (@SuppA Tn A C B A C' B) *)
  intros O P A B C C'; intros.
(* Goal: @SumA Tn C A B' C A B B A B' *)
  apply suma2__or_conga_suppa with A O B; trivial; apply inscribed_angle_1 with P; assumption.
Qed.

(** If the angle ACB is inscribed in a circle of center O and
    C, O lie on opposite sides of AB, then this angle is obtuse. *)

Lemma onc3_ts__obtuse : forall O P A B C,
  OnCircle A O P -> OnCircle B O P -> OnCircle C O P -> TS A B O C ->
  Obtuse A C B.
Proof.
(* Goal: forall (O P A B C : @Tpoint Tn) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @TS Tn A B O C), @Obtuse Tn A C B *)
  intros O P A B C HA HB HC HTS.
(* Goal: @Obtuse Tn A C B *)
  destruct (chord_completion O P C O) as [C' []]; Circle.
(* Goal: @Obtuse Tn A C B *)
  assert (TS A B C C') by (apply bet_ts__ts with O; Side).
(* Goal: @Obtuse Tn A C B *)
  apply (acute_suppa__obtuse A C' B).
(* Goal: @Acute Tn A C' B *)
(* Goal: @SuppA Tn A C' B A C B *)
    apply (onc3_os__acute O P); trivial; exists C; split; Side.
(* Goal: @SuppA Tn A C' B A C B *)
  apply (diam_onc2_ts__suppa O P); Side.
(* Goal: @Diam Tn C' C O P *)
  repeat split; Between.
Qed.

(** Euclid Book III Prop 21:
    In a circle the angles in the same segment are equal to one another. *)

Lemma cop_onc4_os__conga : forall O P A B C C',
  OnCircle A O P -> OnCircle B O P -> OnCircle C O P -> OnCircle C' O P ->
  OS A B C C' -> Coplanar A B C O ->
  CongA A C B A C' B.
Proof.
(* Goal: forall (O P A B C C' : @Tpoint Tn) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @OnCircle Tn C' O P) (_ : @OS Tn A B C C') (_ : @Coplanar Tn A B C O), @CongA Tn A C B A C' B *)
  intros O P A B C C' HA HB HC HC' HOS HCop.
(* Goal: @CongA Tn A C B A C' B *)
  assert_ncols.
(* Goal: @SuppA Tn A C B A C' B *)
  destruct (col_dec A B O).
(* Goal: @eq (@Tpoint Tn) O O' *)
  { assert_diffs.
(* Goal: @SuppA Tn A C B A C' B *)
    assert (Midpoint O A B) by (apply col_onc2__mid with P; auto).
(* Goal: @CongA Tn A C B A C' B *)
    apply l11_16; auto; apply thales_theorem with O; Col; apply cong_transitivity with O P; Cong.
  }
(* Goal: @SuppA Tn A C B A C' B *)
  destruct (cop__one_or_two_sides A B O C); Col; Cop.
  - assert_diffs; destruct (cop2_onc4__or_conga_suppa O P A B C C') as [|Habs]; auto.
(* Goal: @Coplanar Tn A B C' O *)
(* Goal: @OS Tn A B C' D *)
(* Goal: @CongA Tn A C' B A D B *)
      apply coplanar_trans_1 with C; Col; Cop.
(* Goal: @OS Tn A B O O' *)
    exfalso.
(* Goal: False *)
    apply (nlta A C' B), acute_obtuse__lta.
(* Goal: @Acute Tn A C' B *)
(* Goal: @Obtuse Tn A C' B *)
      apply (obtuse_suppa__acute A C B); [apply (onc3_ts__obtuse O P)|]; trivial.
(* Goal: @Obtuse Tn A C' B *)
      apply (onc3_ts__obtuse O P); trivial; apply l9_2, l9_8_2 with C; Side.
  - apply ghalfa2__conga_2 with A O B; apply inscribed_angle with P; trivial.
(* Goal: @OS Tn A B O C' *)
    apply one_side_transitivity with C; Side.
Qed.

(** Euclid Book III Prop 22:
    The opposite angles of quadrilaterals in circles are equal to two right angles. *)

Lemma cop_onc4_ts__suppa : forall O P A B C C',
  OnCircle A O P -> OnCircle B O P -> OnCircle C O P -> OnCircle C' O P ->
  TS A B C C' -> Coplanar A B C O ->
  SuppA A C B A C' B.
Proof.
(* Goal: forall (O P A B C C' : @Tpoint Tn) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @OnCircle Tn C' O P) (_ : @TS Tn A B C C') (_ : @Coplanar Tn A B C O), @SuppA Tn A C B A C' B *)
  intros O P A B C C' HA HB.
(* Goal: forall (_ : @OnCircle Tn C O P) (_ : @OnCircle Tn C' O P) (_ : @TS Tn A B C C') (_ : @Coplanar Tn A B C O), @SuppA Tn A C B A C' B *)
  revert C C'.
  assert (Haux : forall C C', OnCircle C O P -> OnCircle C' O P -> TS A B C C' -> OS A B O C ->
    SuppA A C B A C' B).
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
  { intros C C' HC HC' HTS HOS.
(* Goal: @eq (@Tpoint Tn) O O' *)
    assert_diffs.
(* Goal: @SuppA Tn A C B A C' B *)
    assert (~ Col C A B) by (destruct HTS; assumption).
(* Goal: @SuppA Tn A C B A C' B *)
    assert (Coplanar A B C' O) by (apply coplanar_trans_1 with C; Cop).
(* Goal: @SuppA Tn A C B A C' B *)
    destruct (cop2_onc4__or_conga_suppa O P A B C C') as [Habs|]; Cop.
(* Goal: @OS Tn A B O O' *)
    exfalso.
(* Goal: False *)
    assert (HLta : LtA A C B A C' B); [|destruct HLta as [_ HN]; apply HN, Habs].
(* Goal: @LtA Tn A C B A C' B *)
    apply acute_obtuse__lta.
(* Goal: @SumA Tn C A B' C A B B A B' *)
      apply (onc3_os__acute O P); assumption.
(* Goal: @Obtuse Tn A C' B *)
    apply (onc3_ts__obtuse O P); trivial.
(* Goal: @TS Tn A B O C' *)
    apply l9_8_2 with C; Side.
  }
(* Goal: forall (C C' : @Tpoint Tn) (_ : @OnCircle Tn C O P) (_ : @OnCircle Tn C' O P) (_ : @TS Tn A B C C') (_ : @Coplanar Tn A B C O), @SuppA Tn A C B A C' B *)
  intros C C' HC HC' HTS HCop.
(* Goal: @SuppA Tn A C B A C' B *)
  assert (~ Col C A B) by (destruct HTS; assumption).
(* Goal: @SuppA Tn A C B A C' B *)
  destruct (col_dec A B O).
(* Goal: @eq (@Tpoint Tn) O O' *)
  { assert_diffs.
(* Goal: @SuppA Tn A C B A C' B *)
    assert (Midpoint O A B) by (apply col_onc2__mid with P; auto).
(* Goal: @SuppA Tn A C B A C' B *)
    destruct HTS as [_ []].
(* Goal: @SuppA Tn A C B A C' B *)
    apply per2__suppa; auto; apply thales_theorem with O; Col; apply cong_transitivity with O P; Cong.
  }
(* Goal: @SuppA Tn A C B A C' B *)
  destruct (cop__one_or_two_sides A B O C); Col; Cop.
(* Goal: @SuppA Tn A C B A C' B *)
  apply suppa_sym, Haux; [..|exists C; split]; Side.
Qed.

(** If the angle ACB is acute and inscribed in a circle of center O,
    then C and O lie on the same side of AB. *)

Lemma acute_cop_onc3__os : forall O P A B C, A <> B ->
  OnCircle A O P -> OnCircle B O P -> OnCircle C O P -> Coplanar A B C O -> Acute A C B ->
  OS A B O C.
Proof.
(* Goal: forall (O P A B C : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @Coplanar Tn A B C O) (_ : @Acute Tn A C B), @OS Tn A B O C *)
  intros O P A B C HAB HA HB HC HCop HAcute.
(* Goal: @eq (@Tpoint Tn) O O' *)
  assert_diffs.
(* Goal: @TS Tn A B O C *)
  assert (~ Col A B C) by (apply (onc3__ncol O P); auto).
(* Goal: @TS Tn A B O C *)
  apply coplanar_perm_1 in HCop.
(* Goal: @OS Tn A B O C *)
  apply cop__not_two_sides_one_side; Col; intro Habs; apply (nlta A C B).
  - apply acute_per__lta; auto.
(* Goal: @Per Tn A C B *)
    apply thales_theorem with O; trivial.
(* Goal: not (@Col Tn C O B) *)
(* Goal: not (@Col Tn C' O B) *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T O B) (@Bet Tn C T C')) *)
      apply col_onc2__mid with P; Col.
(* Goal: @SumA Tn C A B' C A B B A B' *)
      apply (onc2__cong O P); assumption.
  - apply acute_obtuse__lta; trivial.
(* Goal: @SumA Tn C A B' C A B B A B' *)
    apply (onc3_ts__obtuse O P); assumption.
Qed.

(** If the angle ACB is obtuse and inscribed in a circle of center O,
    then C and O lie on opposite sides of AB. *)

Lemma cop_obtuse_onc3__ts : forall O P A B C,
  OnCircle A O P -> OnCircle B O P -> OnCircle C O P -> Coplanar A B C O -> Obtuse A C B ->
  TS A B O C.
Proof.
(* Goal: forall (O P A B C : @Tpoint Tn) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @Coplanar Tn A B C O) (_ : @Obtuse Tn A C B), @TS Tn A B O C *)
  intros O P A B C HA HB HC HCop HObtuse.
(* Goal: @eq (@Tpoint Tn) O O' *)
  assert_diffs.
(* Goal: @TS Tn A B O C *)
  assert (~ Col A B C) by (apply (onc3__ncol O P); auto).
(* Goal: @TS Tn A B O C *)
  apply coplanar_perm_1 in HCop.
(* Goal: @TS Tn A B O C *)
  apply cop__not_one_side_two_sides; Col; intro Habs; apply (nlta A C B).
  - apply obtuse_per__lta; auto.
(* Goal: @Per Tn A C B *)
    apply thales_theorem with O; trivial.
(* Goal: not (@Col Tn C O B) *)
(* Goal: not (@Col Tn C' O B) *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T O B) (@Bet Tn C T C')) *)
      apply col_onc2__mid with P; Col.
(* Goal: @SumA Tn C A B' C A B B A B' *)
      apply (onc2__cong O P); assumption.
  - apply acute_obtuse__lta; trivial.
(* Goal: @SumA Tn C A B' C A B B A B' *)
    apply (onc3_os__acute O P); assumption.
Qed.

(** If the angles ACB and ADB are congruent and inscribed in the same circle,
    then C and D lie on the same side of AB. *)

Lemma conga_cop2_onc4__os : forall O P A B C D, ~ Col A B O ->
  OnCircle A O P -> OnCircle B O P -> OnCircle C O P -> OnCircle D O P ->
  Coplanar A B O C -> Coplanar A B O D -> CongA A C B A D B ->
  OS A B C D.
Proof.
(* Goal: forall (O P A B C D : @Tpoint Tn) (_ : not (@Col Tn A B O)) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @OnCircle Tn D O P) (_ : @Coplanar Tn A B O C) (_ : @Coplanar Tn A B O D) (_ : @CongA Tn A C B A D B), @OS Tn A B C D *)
  intros O P A B C D HNCol HA HB HC HD HCopC HCopD HConga.
(* Goal: @eq (@Tpoint Tn) O O' *)
  assert_diffs.
(* Goal: @TS Tn A B C D *)
  destruct (angle_partition A C B) as [HAcute|[HPer|HObtuse]]; auto.
  - apply one_side_transitivity with O; [apply one_side_symmetry|];
(* Goal: @OS Tn A B O C *)
      apply acute_cop_onc3__os with P; Cop.
(* Goal: @SumA Tn C A B' C A B B A B' *)
    apply (acute_conga__acute A C B); assumption.
  - exfalso.
(* Goal: False *)
    apply HNCol, col_permutation_1, midpoint_col.
(* Goal: @eq (@Tpoint Tn) O O' *)
    destruct (midpoint_existence A B) as [M HM].
(* Goal: @Midpoint Tn O A B *)
    assert (M = O); [|subst; apply HM].
(* Goal: @eq (@Tpoint Tn) O O' *)
    assert (HCong := onc2__cong O P).
(* Goal: @eq (@Tpoint Tn) M O *)
    apply (cong4_cop2__eq A C B); Cong; [..|Cop|Cop].
(* Goal: not (@Col Tn A C B) *)
(* Goal: @Cong Tn A M C M *)
      apply per_not_col; auto.
(* Goal: @Cong Tn A M C M *)
      apply cong_commutativity, thales_converse_theorem with B; auto.
  - exists O; split; apply l9_2; apply cop_obtuse_onc3__ts with P; Cop.
(* Goal: @SumA Tn C A B' C A B B A B' *)
    apply (conga_obtuse__obtuse A C B); assumption.
Qed.

(** If the angles ACB and ADB are supplementary and inscribed in the same circle,
    then C and D lie on opposite sides of AB. *)

Lemma cop2_onc4_suppa__ts : forall O P A B C D, ~ Col A B O ->
  OnCircle A O P -> OnCircle B O P -> OnCircle C O P -> OnCircle D O P ->
  Coplanar A B O C -> Coplanar A B O D -> SuppA A C B A D B ->
  TS A B C D.
Proof.
(* Goal: forall (O P A B C D : @Tpoint Tn) (_ : not (@Col Tn A B O)) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @OnCircle Tn D O P) (_ : @Coplanar Tn A B O C) (_ : @Coplanar Tn A B O D) (_ : @SuppA Tn A C B A D B), @TS Tn A B C D *)
  intros O P A B C D HNCol HA HB HC HD HCopC HCopD HSuppa.
(* Goal: @eq (@Tpoint Tn) O O' *)
  assert_diffs.
(* Goal: @TS Tn A B C D *)
  destruct (angle_partition A C B) as [HAcute|[HPer|HObtuse]]; auto.
  - apply l9_8_2 with O.
(* Goal: @SumA Tn C A B' C A B B A B' *)
      apply cop_obtuse_onc3__ts with P; Cop; apply (acute_suppa__obtuse A C B); assumption.
(* Goal: @OS Tn A B O C *)
      apply acute_cop_onc3__os with P; Cop.
  - exfalso.
(* Goal: False *)
    apply HNCol, col_permutation_1, midpoint_col.
(* Goal: @eq (@Tpoint Tn) O O' *)
    destruct (midpoint_existence A B) as [M HM].
(* Goal: @Midpoint Tn O A B *)
    assert (M = O); [|subst; apply HM].
(* Goal: @eq (@Tpoint Tn) O O' *)
    assert (HCong := onc2__cong O P).
(* Goal: @eq (@Tpoint Tn) M O *)
    apply (cong4_cop2__eq A C B); Cong; [..|Cop|Cop].
(* Goal: not (@Col Tn A C B) *)
(* Goal: @Cong Tn A M C M *)
      apply per_not_col; auto.
(* Goal: @Cong Tn A M C M *)
      apply cong_commutativity, thales_converse_theorem with B; auto.
  - apply l9_2, l9_8_2 with O.
(* Goal: @TS Tn A B O C *)
(* Goal: @OS Tn A B O D *)
      apply cop_obtuse_onc3__ts with P; Cop.
(* Goal: @SumA Tn C A B' C A B B A B' *)
    apply acute_cop_onc3__os with P; Cop; apply (obtuse_suppa__acute A C B); assumption.
Qed.

(** Non degenerated triangles can be circumscribed. *)

Lemma triangle_circumscription : forall A B C, ~ Col A B C ->
  exists CC : Tpoint, Cong A CC B CC /\ Cong A CC C CC /\ Coplanar A B C CC.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)), @ex (@Tpoint Tn) (fun CC : @Tpoint Tn => and (@Cong Tn A CC B CC) (and (@Cong Tn A CC C CC) (@Coplanar Tn A B C CC))) *)
  apply postulates_in_euclidean_context; simpl; repeat (try (left; reflexivity); right).
Qed.

(** Euclid Book III Prop 23:
    On the same straight line there cannot be constructed
    two similar and unequal segments of circles on the same side. *)

Lemma conga_cop_onc6_os__eq : forall A B C D O P O' P',
  OnCircle A O P -> OnCircle B O P -> OnCircle C O P -> Coplanar A B C O ->
  OnCircle A O' P' -> OnCircle B O' P' -> OnCircle D O' P' -> Coplanar A B D O' ->
  OS A B C D -> CongA A C B A D B ->
  (O = O' /\ Cong O P O' P').
Proof.
(* Goal: forall (A B C D O P O' P' : @Tpoint Tn) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @Coplanar Tn A B C O) (_ : @OnCircle Tn A O' P') (_ : @OnCircle Tn B O' P') (_ : @OnCircle Tn D O' P') (_ : @Coplanar Tn A B D O') (_ : @OS Tn A B C D) (_ : @CongA Tn A C B A D B), and (@eq (@Tpoint Tn) O O') (@Cong Tn O P O' P') *)
  intros A B C D O P O' P' HA HB HC HCop HA' HB' HD' HCop' HOS HConga.
(* Goal: and (@eq (@Tpoint Tn) O O') (@Cong Tn O P O' P') *)
  assert (O = O'); [|split; trivial; subst O'; apply cong_transitivity with O A; Cong].
(* Goal: @eq (@Tpoint Tn) O O' *)
  assert (HNCol : ~ Col A B C) by (apply one_side_not_col123 with D, HOS).
(* Goal: @eq (@Tpoint Tn) O O' *)
  assert (HCong := onc2__cong O P).
(* Goal: @eq (@Tpoint Tn) O O' *)
  destruct (col_dec A B O) as [|HNCol1].
(* Goal: @eq (@Tpoint Tn) O O' *)
  { assert_diffs.
(* Goal: @eq (@Tpoint Tn) O O' *)
    apply cong2_cop2_onc3__eq with P' A B D; auto; [|apply coplanar_trans_1 with C; Col; Cop].
(* Goal: @Cong Tn O A O D *)
    assert (Midpoint O A B) by (apply col_onc2__mid with P; assumption).
(* Goal: @Cong Tn O A O D *)
    apply thales_converse_theorem with B; auto.
(* Goal: @Per Tn A D B *)
    apply (l11_17 A C B); trivial.
(* Goal: @Per Tn A C B *)
    apply thales_theorem with O; Cong.
  }
(* Goal: @eq (@Tpoint Tn) O O' *)
  assert (HNCol' : ~ Col A B D) by (apply one_side_not_col124 with C, HOS).
(* Goal: @eq (@Tpoint Tn) O O' *)
  assert (HCong' := onc2__cong O' P').
(* Goal: @eq (@Tpoint Tn) O O' *)
  destruct (midpoint_existence A B) as [M HM].
(* Goal: @eq (@Tpoint Tn) O O' *)
  assert (HOS1 : OS A B O O').
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
  { assert_diffs; destruct (angle_partition A C B) as [HAcute|[HPer|HObtuse]]; auto.
    - apply one_side_transitivity with C;
        [|apply one_side_transitivity with D; trivial; apply one_side_symmetry].
(* Goal: @OS Tn A B O C *)
(* Goal: @OS Tn A B O' D *)
        apply acute_cop_onc3__os with P; auto.
(* Goal: @OS Tn A B O' D *)
      apply acute_cop_onc3__os with P'; auto.
(* Goal: @SumA Tn C A B' C A B B A B' *)
      apply (acute_conga__acute A C B); assumption.
    - exfalso.
(* Goal: False *)
      apply HNCol1.
(* Goal: @Col Tn A B O *)
      assert (O = M); [|subst; Col].
(* Goal: @eq (@Tpoint Tn) O M *)
      apply (cong4_cop2__eq A B C); Cong; [|Cop].
(* Goal: @Cong Tn A M C M *)
      apply cong_commutativity, thales_converse_theorem with B; auto.
    - exists C; split; [|apply l9_2, l9_8_2 with D; [apply l9_2|Side]].
(* Goal: @TS Tn A B O C *)
(* Goal: @TS Tn A B O' D *)
        apply cop_obtuse_onc3__ts with P; auto.
(* Goal: @TS Tn A B O' D *)
      apply cop_obtuse_onc3__ts with P'; auto.
(* Goal: @SumA Tn C A B' C A B B A B' *)
      apply (conga_obtuse__obtuse A C B); assumption.
  }
(* Goal: @eq (@Tpoint Tn) O O' *)
  assert (HNCol1' : ~ Col A B O') by (apply one_side_not_col124 with O, HOS1).
(* Goal: @eq (@Tpoint Tn) O O' *)
  destruct (bet_cop_onc2__ex_onc_os_out O P A B C M) as [C1]; Between; Col; [assert_diffs; auto..|].
(* Goal: @eq (@Tpoint Tn) O O' *)
  destruct (bet_cop_onc2__ex_onc_os_out O' P' A B D M) as [D1]; Between; Col; [assert_diffs; auto..|].
(* Goal: @SuppA Tn B A D B C D *)
  spliter.
(* Goal: @eq (@Tpoint Tn) O O' *)
  assert (HNCol2 : ~ Col A B C1) by (apply one_side_not_col124 with C; assumption).
(* Goal: @eq (@Tpoint Tn) O O' *)
  assert (HOut : Out M C1 D1).
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
  { apply (l9_19 A B); [Col| |
      apply one_side_transitivity with C; [|apply one_side_transitivity with D]; Side].
(* Goal: @Col Tn C1 D1 M *)
    assert (O <> M) by (intro; subst; apply HNCol1; Col).
(* Goal: @Col Tn C1 D1 M *)
    assert (O' <> M) by (intro; subst; apply HNCol1'; Col).
(* Goal: @Col Tn C1 D1 M *)
    assert (Col O O' M); [|ColR].
    assert_diffs; apply (cop_per2__col A); auto;
      [|apply mid_onc2__per with P B; auto|apply mid_onc2__per with P' B; auto].
(* Goal: @Coplanar Tn A O O' M *)
    apply coplanar_trans_1 with B; Col; [|Cop].
(* Goal: @Coplanar Tn B A O O' *)
    apply coplanar_trans_1 with C; Col; [Cop|].
(* Goal: @Coplanar Tn C B A O' *)
    apply coplanar_perm_12, coplanar_trans_1 with D; Col; Cop.
  }
(* Goal: @eq (@Tpoint Tn) O O' *)
  destruct (eq_dec_points C1 D1).
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
  { subst D1.
(* Goal: not (@Col Tn C O B) *)
(* Goal: not (@Col Tn C' O B) *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T O B) (@Bet Tn C T C')) *)
    apply (cong4_cop2__eq A B C1); Cong; exists M; left; split; Col.
  }
(* Goal: @eq (@Tpoint Tn) O O' *)
  assert (HNCol2' : ~ Col A B D1) by (apply one_side_not_col124 with D; assumption).
(* Goal: @eq (@Tpoint Tn) O O' *)
  assert (CongA A C1 B A C B) by (apply (cop_onc4_os__conga O P); Side; exists M; left; split; Col).
(* Goal: @eq (@Tpoint Tn) O O' *)
  assert (CongA A D1 B A D B) by (apply (cop_onc4_os__conga O' P'); Side; exists M; left; split; Col).
(* Goal: @eq (@Tpoint Tn) O O' *)
  assert (Out A B M) by (assert_diffs; apply l6_6, bet_out; Between).
(* Goal: @eq (@Tpoint Tn) O O' *)
  assert (Out B A M) by (assert_diffs; apply l6_6, bet_out; Between).
(* Goal: @eq (@Tpoint Tn) O O' *)
  assert (HH := HOut).
(* Goal: @OS Tn A B O O' *)
  destruct HH as [HMC1 [HMD1 [HBet|HBet]]]; exfalso.
  - apply (lta_not_conga A D B A C B); CongA.
(* Goal: @LtA Tn A D B A C B *)
    apply (conga_preserves_lta A D1 B A C1 B); trivial.
(* Goal: @LtA Tn A D1 B A C1 B *)
    assert (Out D1 M C1) by (apply l6_6, bet_out; Between).
    apply os3__lta; [|apply one_side_symmetry, l9_19 with M; Col|];
(* Goal: @OS Tn C B A C' *)
      apply one_side_transitivity with M.
(* Goal: not (@Col Tn C O B) *)
(* Goal: not (@Col Tn C' O B) *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T O B) (@Bet Tn C T C')) *)
      apply invert_one_side, out_one_side; Col.
(* Goal: @OS Tn D1 B M C1 *)
      apply out_one_side; trivial; left; intro; apply HNCol2'; ColR.
(* Goal: not (@Col Tn C O B) *)
(* Goal: not (@Col Tn C' O B) *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T O B) (@Bet Tn C T C')) *)
      apply invert_one_side, out_one_side; Col.
(* Goal: @OS Tn D1 B M C1 *)
      apply out_one_side; trivial; left; intro; apply HNCol2'; ColR.
  - apply (lta_not_conga A C B A D B); trivial.
(* Goal: @LtA Tn A C B A D B *)
    apply (conga_preserves_lta A C1 B A D1 B); trivial.
(* Goal: @LtA Tn A C1 B A D1 B *)
    assert (Out C1 M D1) by (apply l6_6, bet_out; Between).
    apply os3__lta; [|apply l9_19 with M; Col|];
(* Goal: @OS Tn C B A C' *)
      apply one_side_transitivity with M.
(* Goal: not (@Col Tn C O B) *)
(* Goal: not (@Col Tn C' O B) *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T O B) (@Bet Tn C T C')) *)
      apply invert_one_side, out_one_side; Col.
(* Goal: @OS Tn C1 B M D1 *)
      apply out_one_side; trivial; left; intro; apply HNCol2; ColR.
(* Goal: not (@Col Tn C O B) *)
(* Goal: not (@Col Tn C' O B) *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T O B) (@Bet Tn C T C')) *)
      apply invert_one_side, out_one_side; Col.
(* Goal: @OS Tn C1 B M D1 *)
      apply out_one_side; trivial; left; intro; apply HNCol2; ColR.
Qed.

Lemma conga_cop_onc3_os__onc : forall A B C D O P,
  OnCircle A O P -> OnCircle B O P -> OnCircle C O P ->
  Coplanar A B C O -> OS A B C D -> CongA A C B A D B ->
  OnCircle D O P.
Proof.
(* Goal: forall (A B C D O P : @Tpoint Tn) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @Coplanar Tn A B C O) (_ : @OS Tn A B C D) (_ : @CongA Tn A C B A D B), @OnCircle Tn D O P *)
  intros A B C D O P HA HB HC HCop HOS HConga.
(* Goal: @OnCircle Tn D O P *)
  destruct (triangle_circumscription A B D) as [O'].
(* Goal: not (@Col Tn C O B) *)
(* Goal: not (@Col Tn C' O B) *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T O B) (@Bet Tn C T C')) *)
    apply one_side_not_col124 in HOS; Col.
(* Goal: @SuppA Tn B A D B C D *)
  spliter.
(* Goal: @OnCircle Tn D O P *)
  assert (OnCircle A O' A /\ OnCircle B O' A /\ OnCircle D O' A).
(* Goal: and (@OnCircle Tn A O A) (and (@OnCircle Tn B O A) (@OnCircle Tn C O A)) *)
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
    unfold OnCircle; repeat split; Cong.
(* Goal: @SuppA Tn B A D B C D *)
  spliter.
(* Goal: @OnCircle Tn D O P *)
  destruct (conga_cop_onc6_os__eq A B C D O P O' A); trivial.
(* Goal: @OnCircle Tn D O P *)
  subst O'; apply cong_transitivity with O A; Cong.
Qed.

(** If the angles ACB and ADB are congruent and C, D lie on the same side of AB,
    then A, B, C and D are concyclic. *)

Lemma conga_os__ex_circle : forall A B C D,
  OS A B C D -> CongA A C B A D B -> exists O P,
  OnCircle A O P /\ OnCircle B O P /\ OnCircle C O P /\ OnCircle D O P /\ Coplanar A B C O.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @OS Tn A B C D) (_ : @CongA Tn A C B A D B), @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
  intros A B C D HOS HConga.
(* Goal: @SuppA Tn B A D B C D *)
  destruct (triangle_circumscription A B C) as [O]; spliter.
(* Goal: not (@Col Tn A B C) *)
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
    apply one_side_not_col123 with D, HOS.
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
  assert (OnCircle A O A /\ OnCircle B O A /\ OnCircle C O A).
(* Goal: and (@OnCircle Tn A O A) (and (@OnCircle Tn B O A) (@OnCircle Tn C O A)) *)
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
    unfold OnCircle; repeat split; Cong.
(* Goal: @SuppA Tn B A D B C D *)
  spliter.
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
  exists O, A; repeat split; trivial.
(* Goal: @SumA Tn C A B' C A B B A B' *)
  apply (conga_cop_onc3_os__onc A B C); assumption.
Qed.

(** If the angles ACB and ADB are supplementary and C, D lie on opposite sides of AB,
    then A, B, C and D are concyclic. *)

Lemma suppa_ts__ex_circle : forall A B C D,
  TS A B C D -> SuppA A C B A D B -> exists O P,
  OnCircle A O P /\ OnCircle B O P /\ OnCircle C O P /\ OnCircle D O P /\ Coplanar A B C O.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @TS Tn A B C D) (_ : @SuppA Tn A C B A D B), @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
  intros A B.
  assert (Haux : forall C D, TS A B C D -> Obtuse A C B -> SuppA A C B A D B -> exists O P,
    OnCircle A O P /\ OnCircle B O P /\ OnCircle C O P /\ OnCircle D O P /\ Coplanar A B C O).
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
  { intros C D HTS HObtuse HSuppa.
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
    assert (HNCol : ~ Col A B C) by (destruct HTS; Col).
(* Goal: @SuppA Tn B A D B C D *)
    destruct (triangle_circumscription A B C HNCol) as [O]; spliter.
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
    assert (OnCircle A O A /\ OnCircle B O A /\ OnCircle C O A).
(* Goal: and (@OnCircle Tn A O A) (and (@OnCircle Tn B O A) (@OnCircle Tn C O A)) *)
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
      unfold OnCircle; repeat split; Cong.
(* Goal: @SuppA Tn B A D B C D *)
    spliter.
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
    exists O, A; repeat split; trivial.
(* Goal: @OnCircle Tn D O A *)
    destruct (chord_completion O A C O) as [C'[HC' HBet]]; Circle.
(* Goal: @OnCircle Tn D O A *)
    assert (TS A B C C').
(* Goal: @SumA Tn C A B' C A B B A B' *)
      apply bet_ts__ts with O; [apply l9_2, cop_obtuse_onc3__ts with A|]; assumption.
(* Goal: @OnCircle Tn D O A *)
    apply (conga_cop_onc3_os__onc A B C'); trivial.
(* Goal: @Coplanar Tn A B C' O *)
(* Goal: @OS Tn A B C' D *)
(* Goal: @CongA Tn A C' B A D B *)
      apply coplanar_trans_1 with C; Col; Cop.
(* Goal: @OS Tn A B C' D *)
(* Goal: @CongA Tn A C' B A D B *)
      exists C; split; Side.
(* Goal: @SumA Tn C A B' C A B B A B' *)
      apply (suppa2__conga456 A C B); [apply (cop_onc4_ts__suppa O A)|]; assumption.
  }
(* Goal: forall (C D : @Tpoint Tn) (_ : @TS Tn A B C D) (_ : @SuppA Tn A C B A D B), @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
  intros C D HTS HSuppa.
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
  assert_diffs; destruct (angle_partition A C B) as [|[|]]; auto.
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
  { destruct (Haux D C) as [O [P]].
(* Goal: @TS Tn A B D C *)
(* Goal: @Obtuse Tn A D B *)
(* Goal: @SuppA Tn A D B A C B *)
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
      Side.
(* Goal: @Obtuse Tn A D B *)
(* Goal: @SuppA Tn A D B A C B *)
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
      apply (acute_suppa__obtuse A C B); trivial.
(* Goal: @SuppA Tn A D B A C B *)
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
      apply suppa_sym, HSuppa.
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
    exists O, P.
(* Goal: and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))) *)
    spliter; repeat split; trivial.
(* Goal: @Coplanar Tn A B C O *)
    apply coplanar_trans_1 with D; [destruct HTS as [_ []]; Col|Cop..].
  }
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
  destruct (midpoint_existence A B) as [M].
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
  exists M, A.
(* Goal: and (@OnCircle Tn A M A) (and (@OnCircle Tn B M A) (and (@OnCircle Tn C M A) (and (@OnCircle Tn D M A) (@Coplanar Tn A B C M)))) *)
  destruct HTS as [HNCol1 [HNCol2 _]].
  unfold OnCircle; repeat split; [Cong..| | |Cop];
    apply cong_symmetry, thales_converse_theorem with B; auto.
(* Goal: @SumA Tn C A B' C A B B A B' *)
  apply (per_suppa__per A C B); assumption.
Qed.

(** In a convex quadrilateral, if two opposite angles are supplementary
    then the two other angles are also supplementary. *)

Lemma suppa_ts2__suppa : forall A B C D,
  TS A C B D -> TS B D A C -> SuppA A B C A D C -> SuppA B A D B C D.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @TS Tn A C B D) (_ : @TS Tn B D A C) (_ : @SuppA Tn A B C A D C), @SuppA Tn B A D B C D *)
  intros A B C D HTS1 HTS2 HSuppa.
(* Goal: @SuppA Tn B A D B C D *)
  destruct (suppa_ts__ex_circle A C B D) as [O [P]]; trivial.
(* Goal: @SuppA Tn B A D B C D *)
  spliter.
(* Goal: @SuppA Tn B A D B C D *)
  apply (cop_onc4_ts__suppa O P); trivial.
(* Goal: @Coplanar Tn B D A O *)
  apply coplanar_perm_2, coplanar_trans_1 with C; [destruct HTS1; Col|Cop..].
Qed.

End Inscribed_angle.

Section Inscribed_angle_2.

(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
Context `{T2D:Tarski_2D}.
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
Context `{TE:@Tarski_euclidean Tn TnEQD}.

Lemma chord_par_diam : forall O P A B C C' A' U,
 O <> P -> ~Col A B C' -> Diam C C' O P -> Midpoint A' A C' -> OnCircle A O P -> OnCircle B O P ->
 Col A B U -> Perp O U A B -> Par A C' O U -> B = C.
Proof.
intros.
(* Goal: @eq (@Tpoint Tn) O O' *)
assert_diffs.
assert(Midpoint U A B).
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
{
(* Goal: not (@Col Tn C O B) *)
(* Goal: not (@Col Tn C' O B) *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T O B) (@Bet Tn C T C')) *)
  apply(col_onc2_perp__mid O P A B U); Col.
}
assert(O <> A').
(* Goal: not (@Col Tn M O C) *)
intro.
treat_equalities.
induction H7.
apply H7.
(* Goal: @SumA Tn A C B B C O A C O *)
exists O.
(* Goal: not (@Col Tn C O B) *)
(* Goal: not (@Col Tn C' O B) *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T O B) (@Bet Tn C T C')) *)
split; Col.
(* Goal: @SuppA Tn B A D B C D *)
spliter.
assert(Perp A U  O U).
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
{
  apply perp_sym in H6.
(* Goal: not (@Col Tn C O B) *)
(* Goal: not (@Col Tn C' O B) *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T O B) (@Bet Tn C T C')) *)
  apply (perp_col A B O U U); Col.
(* Goal: not (@Col Tn M O C) *)
  intro.
  treat_equalities.
  apply perp_distinct in H6.
  tauto.
}
apply perp_left_comm in H18.
apply perp_not_col in H18.
(* Goal: not (@Col Tn C O B) *)
(* Goal: not (@Col Tn C' O B) *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T O B) (@Bet Tn C T C')) *)
apply H18; Col.
unfold Diam in H1.
(* Goal: @SuppA Tn B A D B C D *)
spliter.
assert(HH:=mid_onc2__perp O P A C' A' H15 H13 H3 H17 H2).
assert(Perp O U O A').
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
{
  apply(par_perp__perp A C' O U O A' H7); Perp.
}

assert(Par O A' A B).
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
{
  apply (l12_9_2D _ _ _ _ O U); Perp.
}
assert(HM:=midpoint_existence B C').
ex_and HM O'.
assert(HP:= triangle_mid_par A B C' O' A' H0 H20 H2).
apply par_strict_par in HP.
assert(Par O A' A' O').
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
{
  apply (par_trans _ _ A B); Par.
}
assert(Col O O' A').
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
{
  induction H21.
  apply False_ind.
  apply H21.
  exists A'.
(* Goal: not (@Col Tn C O B) *)
(* Goal: not (@Col Tn C' O B) *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T O B) (@Bet Tn C T C')) *)
  split; Col.
(* Goal: @SuppA Tn B A D B C D *)
  spliter.
(* Goal: not (@Col Tn C O B) *)
(* Goal: not (@Col Tn C' O B) *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T O B) (@Bet Tn C T C')) *)
  Col.
}

induction(eq_dec_points O O').
treat_equalities.
eapply(symmetric_point_uniqueness C' O); Midpoint.
split; eCong.
Between.

assert(HQ:= mid_onc2__perp O P B C' O' H23  H10 H4 H17 H20).
(* Goal: not (@Col Tn C O B) *)
(* Goal: not (@Col Tn C' O B) *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T O B) (@Bet Tn C T C')) *)
apply(perp_col O A' A C' O') in HH; Col.
assert(Par A C' B C').
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@OnCircle Tn D O P) (@Coplanar Tn A B C O)))))) *)
{
  apply(l12_9_2D A C' B C' O O'); Perp.
}
apply False_ind.
induction H24.
apply H24.
(* Goal: @SumA Tn A O B B O C' A O C' *)
exists C'.
(* Goal: not (@Col Tn C O B) *)
(* Goal: not (@Col Tn C' O B) *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T O B) (@Bet Tn C T C')) *)
split;Col.
(* Goal: @SuppA Tn B A D B C D *)
spliter.
apply H0.
(* Goal: not (@Col Tn C O B) *)
(* Goal: not (@Col Tn C' O B) *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T O B) (@Bet Tn C T C')) *)
Col.
Qed.

End Inscribed_angle_2.
