Require Import GeoCoq.Tactics.Coinc.tactics_axioms.
Require Import GeoCoq.Tarski_dev.Annexes.inscribed_angle.

Section Tarski_is_a_Coinc_theory_for_concyclic.

Context `{TE:Tarski_euclidean}.

Definition not_col : arity Tpoint 3 := fun A B C : Tpoint => ~ Col A B C.

Lemma not_col_perm_1 : forall A X, app_1_n not_col A X -> app_n_1 not_col X A.
(* Goal: forall (A : @Tpoint Tn) (X : cartesianPower (@Tpoint Tn) (S (S O))) (_ : @app_1_n (@Tpoint Tn) (S (S O)) not_col A X), @app_n_1 (@Tpoint Tn) (S (S O)) not_col X A *)
Proof. unfold not_col; simpl; Col. Qed.

Lemma not_col_perm_2 : forall A B (X : cartesianPower Tpoint 1),
  app_2_n not_col A B X -> app_2_n not_col B A X.
Proof. unfold not_col, app_2_n; simpl; Col. Qed.

Lemma concyclic_aux : forall A B C D, Concyclic A B C D -> 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) (_ : @Concyclic Tn A B C D), @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 [HCop [O1 [P1]]]; 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)))))) *)
  destruct (col_dec 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)))))) *)
(* 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 O1, P1; repeat split; 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 (l11_62_existence A B C O1) as [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)))))) *)
  exists O, A.
(* Goal: and (@OnCircle Tn A O A) (and (@OnCircle Tn B O A) (and (@OnCircle Tn C O A) (and (@OnCircle Tn D O A) (@Coplanar Tn A B C O)))) *)
  assert (HCong := onc2__cong O1 P1).
(* Goal: and (@OnCircle Tn A O A) (and (@OnCircle Tn B O A) (and (@OnCircle Tn C O A) (and (@OnCircle Tn D O A) (@Coplanar Tn A B C O)))) *)
  repeat split; [Circle|apply cong2_per2__cong with O1 O1; Cop; Cong..|assumption].
Qed.

Definition Concyclic_gen A B C D :=
  Concyclic A B C D \/ (Col A B C /\ Col A B D /\ Col A C D /\ Col B C D).

Definition concy : arity Tpoint 4 := Concyclic_gen.

Lemma concyclic_gen_2341 : forall A B C D,
  Concyclic_gen A B C D -> Concyclic_gen B C D A.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : Concyclic_gen A B C D), Concyclic_gen B A C D *)
unfold Concyclic_gen; simpl; intros A B C D H.
elim H; clear H; intro H;
[left; destruct H as [HCop [O [P]]]; split; Cop; exists O, P|right]; spliter; repeat split; Col.
Qed.

Lemma concy_perm_1 : forall (A : Tpoint) (X : cartesianPower Tpoint 3),
app_1_n concy A X -> app_n_1 concy X A.
Proof. unfold concy; simpl. intros; apply concyclic_gen_2341; auto. Qed.

Lemma concyclic_gen_2134 : forall A B C D,
  Concyclic_gen A B C D -> Concyclic_gen B A C D.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : Concyclic_gen A B C D), Concyclic_gen B A C D *)
unfold Concyclic_gen; simpl; intros A B C D H.
elim H; clear H; intro H;
[left; destruct H as [HCop [O [P]]]; split; Cop; exists O, P|right]; spliter; repeat split; Col.
Qed.

Lemma concy_perm_2 : forall (A B : Tpoint) (X : cartesianPower Tpoint 2),
app_2_n concy A B X -> app_2_n concy B A X.
Proof.
(* Goal: forall (A B : @Tpoint Tn) (X : cartesianPower (@Tpoint Tn) (S (S O))) (_ : @app_2_n (@Tpoint Tn) (S (S O)) concy A B X), @app_2_n (@Tpoint Tn) (S (S O)) concy B A X *)
unfold app_2_n, concy; simpl; intros; apply concyclic_gen_2134; auto.
Qed.

Lemma concyclic_gen_1123 : forall A B C, Concyclic_gen A A B C.
Proof.
(* Goal: forall A B C : @Tpoint Tn, Concyclic_gen A A B C *)
unfold Concyclic_gen; simpl; intros A B C.
(* Goal: or (@Concyclic Tn A A B C) (and (@Col Tn A A B) (and (@Col Tn A A C) (and (@Col Tn A B C) (@Col Tn A B C)))) *)
elim (col_dec A B C); intro; [right; repeat split; Col|].
(* Goal: or (@Concyclic Tn Q R A B) (and (@Col Tn Q R A) (and (@Col Tn Q R B) (and (@Col Tn Q A B) (@Col Tn R A B)))) *)
left.
(* Goal: @Concyclic Tn A A B C *)
split; 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 A O P) (and (@OnCircle Tn B O P) (@OnCircle Tn C O P))))) *)
destruct (triangle_circumscription A B C H) 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 A O P) (and (@OnCircle Tn B O P) (@OnCircle Tn C O P))))) *)
exists O, A; unfold OnCircle; repeat split; Cong.
Qed.

Lemma concy_bd : forall (A : Tpoint) (X  : cartesianPower Tpoint 2),
app_2_n concy A A X.
Proof. unfold app_2_n, concy; simpl; intros; apply concyclic_gen_1123. Qed.

Lemma concy_trans_1 : forall P Q R A B,
  ~Col P Q R ->
  Concyclic_gen P Q R A -> Concyclic_gen P Q R B ->
  Concyclic_gen Q R A B.
Proof.
(* Goal: forall (P Q R A B : @Tpoint Tn) (_ : not (@Col Tn P Q R)) (_ : Concyclic_gen P Q R A) (_ : Concyclic_gen P Q R B), Concyclic_gen Q R A B *)
unfold Concyclic_gen; intros P Q R A B HNC H1 H2.
(* Goal: or (@Concyclic Tn Q R A B) (and (@Col Tn Q R A) (and (@Col Tn Q R B) (and (@Col Tn Q A B) (@Col Tn R A B)))) *)
elim H1; clear H1; intro H1; [|spliter; exfalso; apply HNC; Col].
(* Goal: or (@Concyclic Tn Q R A B) (and (@Col Tn Q R A) (and (@Col Tn Q R B) (and (@Col Tn Q A B) (@Col Tn R A B)))) *)
elim H2; clear H2; intro H2; [|spliter; exfalso; apply HNC; Col].
(* Goal: or (@Concyclic Tn Q R A B) (and (@Col Tn Q R A) (and (@Col Tn Q R B) (and (@Col Tn Q A B) (@Col Tn R A B)))) *)
destruct (concyclic_aux P Q R A H1) as [O [M]].
(* Goal: or (@Concyclic Tn Q R A B) (and (@Col Tn Q R A) (and (@Col Tn Q R B) (and (@Col Tn Q A B) (@Col Tn R A B)))) *)
destruct (concyclic_aux P Q R B H2) as [O' [M']].
(* Goal: or (@Concyclic Tn Q R A B) (and (@Col Tn Q R A) (and (@Col Tn Q R B) (and (@Col Tn Q A B) (@Col Tn R A B)))) *)
spliter.
(* Goal: or (@Concyclic Tn Q R A B) (and (@Col Tn Q R A) (and (@Col Tn Q R B) (and (@Col Tn Q A B) (@Col Tn R A B)))) *)
assert (O = O').
  apply (cong4_cop2__eq P Q R); trivial;
  [apply cong_transitivity with O M..|
   apply cong_transitivity with O' M'|apply cong_transitivity with O' M']; Cong.
(* Goal: or (@Concyclic Tn Q R A B) (and (@Col Tn Q R A) (and (@Col Tn Q R B) (and (@Col Tn Q A B) (@Col Tn R A B)))) *)
subst O'.
(* Goal: or (@Concyclic Tn Q R A B) (and (@Col Tn Q R A) (and (@Col Tn Q R B) (and (@Col Tn Q A B) (@Col Tn R A B)))) *)
assert (OnCircle B O M).
(* Goal: @OnCircle Tn B O M *)
(* Goal: or (@Concyclic Tn Q R A B) (and (@Col Tn Q R A) (and (@Col Tn Q R B) (and (@Col Tn Q A B) (@Col Tn R A B)))) *)
  apply cong_transitivity with O M'; [|apply cong_transitivity with O P]; Cong.
(* Goal: or (@Concyclic Tn Q R A B) (and (@Col Tn Q R A) (and (@Col Tn Q R B) (and (@Col Tn Q A B) (@Col Tn R A B)))) *)
clear dependent M'.
(* Goal: or (@Concyclic Tn Q R A B) (and (@Col Tn Q R A) (and (@Col Tn Q R B) (and (@Col Tn Q A B) (@Col Tn R A B)))) *)
destruct H1 as [HCop1 _].
(* Goal: or (@Concyclic Tn Q R A B) (and (@Col Tn Q R A) (and (@Col Tn Q R B) (and (@Col Tn Q A B) (@Col Tn R A B)))) *)
destruct H2 as [HCop2 _].
(* Goal: or (@Concyclic Tn Q R A B) (and (@Col Tn Q R A) (and (@Col Tn Q R B) (and (@Col Tn Q A B) (@Col Tn R A B)))) *)
left.
(* Goal: @Concyclic Tn Q R A B *)
split.
(* Goal: @Coplanar Tn Q R A B *)
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn Q O P) (and (@OnCircle Tn R O P) (and (@OnCircle Tn A O P) (@OnCircle Tn B O P))))) *)
  apply coplanar_trans_1 with P; Col; Cop.
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@OnCircle Tn Q O P) (and (@OnCircle Tn R O P) (and (@OnCircle Tn A O P) (@OnCircle Tn B O P))))) *)
exists O, M; repeat split; assumption.
Qed.

Lemma concyclic_gen_pseudo_trans : forall A B C D P Q R,
  ~ Col P Q R ->
  Concyclic_gen P Q R A ->
  Concyclic_gen P Q R B ->
  Concyclic_gen P Q R C ->
  Concyclic_gen P Q R D ->
  Concyclic_gen A B C D.
Proof.
(* Goal: forall (A B C D P Q R : @Tpoint Tn) (_ : not (@Col Tn P Q R)) (_ : Concyclic_gen P Q R A) (_ : Concyclic_gen P Q R B) (_ : Concyclic_gen P Q R C) (_ : Concyclic_gen P Q R D), Concyclic_gen A B C D *)
intros A B C D P Q R HNC HConcy1 HConcy2 HConcy3 HConcy4.
(* Goal: Concyclic_gen A B C D *)
elim (col_dec R A B); intro HRAB.

(* Goal: Concyclic_gen A B C D *)
  {
(* Goal: Concyclic_gen A B C D *)
  elim (col_dec R C D); intro HRCD.

(* Goal: Concyclic_gen A B C D *)
    {
(* Goal: Concyclic_gen A B C D *)
    elim (col_dec Q A B); intro HQAB.

(* Goal: Concyclic_gen A B C D *)
      {
(* Goal: Concyclic_gen A B C D *)
      elim (eq_dec_points A B); intro HAB; try (subst A; apply concyclic_gen_1123).
(* Goal: Concyclic_gen A B C D *)
      assert (HPAB : ~ Col P A B) by (intro; apply HNC; ColR).
(* Goal: Concyclic_gen A B C D *)
      elim (col_dec P Q A); intro HPQA.

(* Goal: Concyclic_gen A B C D *)
        {
(* Goal: Concyclic_gen A B C D *)
        assert (HQRB : ~ Col P Q B) by (intro; assert_diffs; apply HPAB; ColR).
(* Goal: Concyclic_gen A B C D *)
        assert (HNC' : ~ Col R P Q) by Col.
        assert (H : forall A B C D, Concyclic_gen A B C D ->
                                    Concyclic_gen C A B D).
(* Goal: Concyclic_gen A B C D *)
          {
(* Goal: forall (A B C D : @Tpoint Tn) (_ : Concyclic_gen A B C D), Concyclic_gen C A B D *)
          intros; apply concyclic_gen_2341; apply concyclic_gen_2134.
(* Goal: Concyclic_gen A B C D *)
          do 2 apply concyclic_gen_2341; auto.
          }
(* Goal: Concyclic_gen A B C D *)
        apply H in HConcy1; apply H in HConcy2.
(* Goal: Concyclic_gen A B C D *)
        apply H in HConcy3; apply H in HConcy4.
(* Goal: Concyclic_gen A B C D *)
        assert (HConcy5 := concy_trans_1 R P Q B A HNC' HConcy2 HConcy1).
(* Goal: Concyclic_gen A B C D *)
        assert (HConcy6 := concy_trans_1 R P Q B C HNC' HConcy2 HConcy3).
(* Goal: Concyclic_gen A B C D *)
        assert (HConcy7 := concy_trans_1 R P Q B D HNC' HConcy2 HConcy4).
(* Goal: Concyclic_gen A B C D *)
        assert (HQPB : ~ Col Q P B) by Col.
(* Goal: Concyclic_gen A B C D *)
        apply concyclic_gen_2134 in HConcy5.
(* Goal: Concyclic_gen A B C D *)
        apply concyclic_gen_2134 in HConcy6.
(* Goal: Concyclic_gen A B C D *)
        apply concyclic_gen_2134 in HConcy7.
(* Goal: Concyclic_gen A B C D *)
        assert (HConcy8 := concy_trans_1 Q P B A C HQPB HConcy5 HConcy6).
(* Goal: Concyclic_gen A B C D *)
        assert (HConcy9 := concy_trans_1 Q P B A D HQPB HConcy5 HConcy7).
(* Goal: Concyclic_gen A B C D *)
        assert (HRBA : ~ Col P B A) by Col.
(* Goal: Concyclic_gen A B C D *)
        assert (HConcy := concy_trans_1 P B A C D HRBA HConcy8 HConcy9).
(* Goal: Concyclic_gen A B C D *)
        apply concyclic_gen_2134; auto.
        }

(* Goal: Concyclic_gen A B C D *)
        {
(* Goal: Concyclic_gen A B C D *)
        assert (HNC' : ~ Col R P Q) by Col.
        assert (H : forall A B C D, Concyclic_gen A B C D ->
                                    Concyclic_gen C A B D).
(* Goal: Concyclic_gen A B C D *)
          {
(* Goal: forall (A B C D : @Tpoint Tn) (_ : Concyclic_gen A B C D), Concyclic_gen C A B D *)
          intros; apply concyclic_gen_2341; apply concyclic_gen_2134.
(* Goal: Concyclic_gen A B C D *)
          do 2 apply concyclic_gen_2341; auto.
          }
(* Goal: Concyclic_gen A B C D *)
        apply H in HConcy1; apply H in HConcy2.
(* Goal: Concyclic_gen A B C D *)
        apply H in HConcy3; apply H in HConcy4.
(* Goal: Concyclic_gen A B C D *)
        assert (HConcy5 := concy_trans_1 R P Q A B HNC' HConcy1 HConcy2).
(* Goal: Concyclic_gen A B C D *)
        assert (HConcy6 := concy_trans_1 R P Q A C HNC' HConcy1 HConcy3).
(* Goal: Concyclic_gen A B C D *)
        assert (HConcy7 := concy_trans_1 R P Q A D HNC' HConcy1 HConcy4).
(* Goal: Concyclic_gen A B C D *)
        assert (HQPA : ~ Col Q P A) by Col.
(* Goal: Concyclic_gen A B C D *)
        apply concyclic_gen_2134 in HConcy5.
(* Goal: Concyclic_gen A B C D *)
        apply concyclic_gen_2134 in HConcy6.
(* Goal: Concyclic_gen A B C D *)
        apply concyclic_gen_2134 in HConcy7.
(* Goal: Concyclic_gen A B C D *)
        assert (HConcy8 := concy_trans_1 Q P A B C HQPA HConcy5 HConcy6).
(* Goal: Concyclic_gen A B C D *)
        assert (HConcy9 := concy_trans_1 Q P A B D HQPA HConcy5 HConcy7).
(* Goal: Concyclic_gen A B C D *)
        assert (HConcy := concy_trans_1 P A B C D HPAB HConcy8 HConcy9).
(* Goal: Concyclic_gen A B C D *)
        auto.
        }
      }

(* Goal: Concyclic_gen A B C D *)
      {
(* Goal: Concyclic_gen A B C D *)
      elim (col_dec P Q A); intro HPQA.

(* Goal: Concyclic_gen A B C D *)
        {
(* Goal: Concyclic_gen A B C D *)
        assert (HPQB : ~ Col P Q B) by (intro; assert_diffs; apply HQAB; ColR).
(* Goal: Concyclic_gen A B C D *)
        assert (HNC' : ~ Col R P Q) by Col.
        assert (H : forall A B C D, Concyclic_gen A B C D ->
                                    Concyclic_gen C A B D).
(* Goal: Concyclic_gen A B C D *)
          {
(* Goal: forall (A B C D : @Tpoint Tn) (_ : Concyclic_gen A B C D), Concyclic_gen C A B D *)
          intros; apply concyclic_gen_2341; apply concyclic_gen_2134.
(* Goal: Concyclic_gen A B C D *)
          do 2 apply concyclic_gen_2341; auto.
          }
(* Goal: Concyclic_gen A B C D *)
        apply H in HConcy1; apply H in HConcy2.
(* Goal: Concyclic_gen A B C D *)
        apply H in HConcy3; apply H in HConcy4.
(* Goal: Concyclic_gen A B C D *)
        assert (HConcy5 := concy_trans_1 R P Q B A HNC' HConcy2 HConcy1).
(* Goal: Concyclic_gen A B C D *)
        assert (HConcy6 := concy_trans_1 R P Q B C HNC' HConcy2 HConcy3).
(* Goal: Concyclic_gen A B C D *)
        assert (HConcy7 := concy_trans_1 R P Q B D HNC' HConcy2 HConcy4).
(* Goal: Concyclic_gen A B C D *)
        assert (HConcy8 := concy_trans_1 P Q B A C HPQB HConcy5 HConcy6).
(* Goal: Concyclic_gen A B C D *)
        assert (HConcy9 := concy_trans_1 P Q B A D HPQB HConcy5 HConcy7).
(* Goal: Concyclic_gen A B C D *)
        assert (HQBA : ~ Col Q B A) by Col.
(* Goal: Concyclic_gen A B C D *)
        assert (HConcy := concy_trans_1 Q B A C D HQBA HConcy8 HConcy9).
(* Goal: Concyclic_gen A B C D *)
        apply concyclic_gen_2134; auto.
        }

(* Goal: Concyclic_gen A B C D *)
        {
(* Goal: Concyclic_gen A B C D *)
        assert (HNC' : ~ Col R P Q) by Col.
        assert (H : forall A B C D, Concyclic_gen A B C D ->
                                    Concyclic_gen C A B D).
(* Goal: Concyclic_gen A B C D *)
          {
(* Goal: forall (A B C D : @Tpoint Tn) (_ : Concyclic_gen A B C D), Concyclic_gen C A B D *)
          intros; apply concyclic_gen_2341; apply concyclic_gen_2134.
(* Goal: Concyclic_gen A B C D *)
          do 2 apply concyclic_gen_2341; auto.
          }
(* Goal: Concyclic_gen A B C D *)
        apply H in HConcy1; apply H in HConcy2.
(* Goal: Concyclic_gen A B C D *)
        apply H in HConcy3; apply H in HConcy4.
(* Goal: Concyclic_gen A B C D *)
        assert (HConcy5 := concy_trans_1 R P Q A B HNC' HConcy1 HConcy2).
(* Goal: Concyclic_gen A B C D *)
        assert (HConcy6 := concy_trans_1 R P Q A C HNC' HConcy1 HConcy3).
(* Goal: Concyclic_gen A B C D *)
        assert (HConcy7 := concy_trans_1 R P Q A D HNC' HConcy1 HConcy4).
(* Goal: Concyclic_gen A B C D *)
        assert (HConcy8 := concy_trans_1 P Q A B C HPQA HConcy5 HConcy6).
(* Goal: Concyclic_gen A B C D *)
        assert (HConcy9 := concy_trans_1 P Q A B D HPQA HConcy5 HConcy7).
(* Goal: Concyclic_gen A B C D *)
        assert (HConcy := concy_trans_1 Q A B C D HQAB HConcy8 HConcy9).
(* Goal: Concyclic_gen A B C D *)
        auto.
        }
      }
    }

(* Goal: Concyclic_gen A B C D *)
    {
(* Goal: Concyclic_gen A B C D *)
    elim (col_dec Q R C); intro HQRC.

(* Goal: Concyclic_gen A B C D *)
      {
(* Goal: Concyclic_gen A B C D *)
      assert (HQRD : ~ Col Q R D) by (intro; assert_diffs; apply HRCD; ColR).
(* Goal: Concyclic_gen A B C D *)
      assert (HConcy5 := concy_trans_1 P Q R D A HNC HConcy4 HConcy1).
(* Goal: Concyclic_gen A B C D *)
      assert (HConcy6 := concy_trans_1 P Q R D B HNC HConcy4 HConcy2).
(* Goal: Concyclic_gen A B C D *)
      assert (HConcy7 := concy_trans_1 P Q R D C HNC HConcy4 HConcy3).
(* Goal: Concyclic_gen A B C D *)
      assert (HConcy8 := concy_trans_1 Q R D C A HQRD HConcy7 HConcy5).
(* Goal: Concyclic_gen A B C D *)
      assert (HConcy9 := concy_trans_1 Q R D C B HQRD HConcy7 HConcy6).
(* Goal: Concyclic_gen A B C D *)
      assert (HRDC : ~ Col R D C) by Col.
(* Goal: Concyclic_gen A B C D *)
      assert (HConcy := concy_trans_1 R D C A B HRDC HConcy8 HConcy9).
(* Goal: Concyclic_gen A B C D *)
      do 2 apply concyclic_gen_2341; apply concyclic_gen_2134; auto.
      }

(* Goal: Concyclic_gen A B C D *)
      {
(* Goal: Concyclic_gen A B C D *)
      assert (HConcy5 := concy_trans_1 P Q R C A HNC HConcy3 HConcy1).
(* Goal: Concyclic_gen A B C D *)
      assert (HConcy6 := concy_trans_1 P Q R C B HNC HConcy3 HConcy2).
(* Goal: Concyclic_gen A B C D *)
      assert (HConcy7 := concy_trans_1 P Q R C D HNC HConcy3 HConcy4).
(* Goal: Concyclic_gen A B C D *)
      assert (HConcy8 := concy_trans_1 Q R C D A HQRC HConcy7 HConcy5).
(* Goal: Concyclic_gen A B C D *)
      assert (HConcy9 := concy_trans_1 Q R C D B HQRC HConcy7 HConcy6).
(* Goal: Concyclic_gen A B C D *)
      assert (HConcy := concy_trans_1 R C D A B HRCD HConcy8 HConcy9).
(* Goal: Concyclic_gen A B C D *)
      do 2 apply concyclic_gen_2341; auto.
      }
    }
  }

(* Goal: Concyclic_gen A B C D *)
  {
(* Goal: Concyclic_gen A B C D *)
  elim (col_dec Q R A); intro HQRA.

(* Goal: Concyclic_gen A B C D *)
    {
(* Goal: Concyclic_gen A B C D *)
    assert (HQRB : ~ Col Q R B) by (intro; assert_diffs; apply HRAB; ColR).
(* Goal: Concyclic_gen A B C D *)
    assert (HConcy5 := concy_trans_1 P Q R B A HNC HConcy2 HConcy1).
(* Goal: Concyclic_gen A B C D *)
    assert (HConcy6 := concy_trans_1 P Q R B C HNC HConcy2 HConcy3).
(* Goal: Concyclic_gen A B C D *)
    assert (HConcy7 := concy_trans_1 P Q R B D HNC HConcy2 HConcy4).
(* Goal: Concyclic_gen A B C D *)
    assert (HConcy8 := concy_trans_1 Q R B A C HQRB HConcy5 HConcy6).
(* Goal: Concyclic_gen A B C D *)
    assert (HConcy9 := concy_trans_1 Q R B A D HQRB HConcy5 HConcy7).
(* Goal: Concyclic_gen A B C D *)
    assert (HRBA : ~ Col R B A) by Col.
(* Goal: Concyclic_gen A B C D *)
    assert (HConcy := concy_trans_1 R B A C D HRBA HConcy8 HConcy9).
(* Goal: Concyclic_gen A B C D *)
    apply concyclic_gen_2134; auto.
    }

(* Goal: Concyclic_gen A B C D *)
    {
(* Goal: Concyclic_gen A B C D *)
    assert (HConcy5 := concy_trans_1 P Q R A B HNC HConcy1 HConcy2).
(* Goal: Concyclic_gen A B C D *)
    assert (HConcy6 := concy_trans_1 P Q R A C HNC HConcy1 HConcy3).
(* Goal: Concyclic_gen A B C D *)
    assert (HConcy7 := concy_trans_1 P Q R A D HNC HConcy1 HConcy4).
(* Goal: Concyclic_gen A B C D *)
    assert (HConcy8 := concy_trans_1 Q R A B C HQRA HConcy5 HConcy6).
(* Goal: Concyclic_gen A B C D *)
    assert (HConcy9 := concy_trans_1 Q R A B D HQRA HConcy5 HConcy7).
(* Goal: Concyclic_gen A B C D *)
    assert (HConcy := concy_trans_1 R A B C D HRAB HConcy8 HConcy9).
(* Goal: Concyclic_gen A B C D *)
    auto.
    }
  }
Qed.

Lemma concy_3 :
  forall (CONCY : cartesianPower Tpoint 4) (NOT_COL : cartesianPower Tpoint 3),
  pred_conj concy CONCY NOT_COL -> app not_col NOT_COL -> app concy CONCY.
Proof.
(* Goal: forall (CONCY : cartesianPower (@Tpoint Tn) (S (S (S (S O))))) (NOT_COL : cartesianPower (@Tpoint Tn) (S (S (S O)))) (_ : @pred_conj (@Tpoint Tn) (S (S (S O))) concy CONCY NOT_COL) (_ : @app (@Tpoint Tn) (S (S (S O))) not_col NOT_COL), @app (@Tpoint Tn) (S (S (S (S O)))) concy CONCY *)
unfold pred_conj, app_2_n, concy; simpl.
(* Goal: forall (CONCY : cartesianPower (@Tpoint Tn) (S (S (S (S O))))) (NOT_COL : cartesianPower (@Tpoint Tn) (S (S (S O)))) (_ : and (Concyclic_gen (@fst (@Tpoint Tn) (prod (@Tpoint Tn) (prod (@Tpoint Tn) (@Tpoint Tn))) CONCY) (@fst (@Tpoint Tn) (prod (@Tpoint Tn) (@Tpoint Tn)) NOT_COL) (@fst (@Tpoint Tn) (@Tpoint Tn) (@snd (@Tpoint Tn) (prod (@Tpoint Tn) (@Tpoint Tn)) NOT_COL)) (@snd (@Tpoint Tn) (@Tpoint Tn) (@snd (@Tpoint Tn) (prod (@Tpoint Tn) (@Tpoint Tn)) NOT_COL))) (and (Concyclic_gen (@fst (@Tpoint Tn) (prod (@Tpoint Tn) (@Tpoint Tn)) (@snd (@Tpoint Tn) (prod (@Tpoint Tn) (prod (@Tpoint Tn) (@Tpoint Tn))) CONCY)) (@fst (@Tpoint Tn) (prod (@Tpoint Tn) (@Tpoint Tn)) NOT_COL) (@fst (@Tpoint Tn) (@Tpoint Tn) (@snd (@Tpoint Tn) (prod (@Tpoint Tn) (@Tpoint Tn)) NOT_COL)) (@snd (@Tpoint Tn) (@Tpoint Tn) (@snd (@Tpoint Tn) (prod (@Tpoint Tn) (@Tpoint Tn)) NOT_COL))) (and (Concyclic_gen (@fst (@Tpoint Tn) (@Tpoint Tn) (@snd (@Tpoint Tn) (prod (@Tpoint Tn) (@Tpoint Tn)) (@snd (@Tpoint Tn) (prod (@Tpoint Tn) (prod (@Tpoint Tn) (@Tpoint Tn))) CONCY))) (@fst (@Tpoint Tn) (prod (@Tpoint Tn) (@Tpoint Tn)) NOT_COL) (@fst (@Tpoint Tn) (@Tpoint Tn) (@snd (@Tpoint Tn) (prod (@Tpoint Tn) (@Tpoint Tn)) NOT_COL)) (@snd (@Tpoint Tn) (@Tpoint Tn) (@snd (@Tpoint Tn) (prod (@Tpoint Tn) (@Tpoint Tn)) NOT_COL))) (Concyclic_gen (@snd (@Tpoint Tn) (@Tpoint Tn) (@snd (@Tpoint Tn) (prod (@Tpoint Tn) (@Tpoint Tn)) (@snd (@Tpoint Tn) (prod (@Tpoint Tn) (prod (@Tpoint Tn) (@Tpoint Tn))) CONCY))) (@fst (@Tpoint Tn) (prod (@Tpoint Tn) (@Tpoint Tn)) NOT_COL) (@fst (@Tpoint Tn) (@Tpoint Tn) (@snd (@Tpoint Tn) (prod (@Tpoint Tn) (@Tpoint Tn)) NOT_COL)) (@snd (@Tpoint Tn) (@Tpoint Tn) (@snd (@Tpoint Tn) (prod (@Tpoint Tn) (@Tpoint Tn)) NOT_COL)))))) (_ : not_col (@fst (@Tpoint Tn) (prod (@Tpoint Tn) (@Tpoint Tn)) NOT_COL) (@fst (@Tpoint Tn) (@Tpoint Tn) (@snd (@Tpoint Tn) (prod (@Tpoint Tn) (@Tpoint Tn)) NOT_COL)) (@snd (@Tpoint Tn) (@Tpoint Tn) (@snd (@Tpoint Tn) (prod (@Tpoint Tn) (@Tpoint Tn)) NOT_COL))), Concyclic_gen (@fst (@Tpoint Tn) (prod (@Tpoint Tn) (prod (@Tpoint Tn) (@Tpoint Tn))) CONCY) (@fst (@Tpoint Tn) (prod (@Tpoint Tn) (@Tpoint Tn)) (@snd (@Tpoint Tn) (prod (@Tpoint Tn) (prod (@Tpoint Tn) (@Tpoint Tn))) CONCY)) (@fst (@Tpoint Tn) (@Tpoint Tn) (@snd (@Tpoint Tn) (prod (@Tpoint Tn) (@Tpoint Tn)) (@snd (@Tpoint Tn) (prod (@Tpoint Tn) (prod (@Tpoint Tn) (@Tpoint Tn))) CONCY))) (@snd (@Tpoint Tn) (@Tpoint Tn) (@snd (@Tpoint Tn) (prod (@Tpoint Tn) (@Tpoint Tn)) (@snd (@Tpoint Tn) (prod (@Tpoint Tn) (prod (@Tpoint Tn) (@Tpoint Tn))) CONCY))) *)
intros CONCY NOT_COL HConcy HNot_Col.
(* Goal: Concyclic_gen (@fst (@Tpoint Tn) (prod (@Tpoint Tn) (prod (@Tpoint Tn) (@Tpoint Tn))) CONCY) (@fst (@Tpoint Tn) (prod (@Tpoint Tn) (@Tpoint Tn)) (@snd (@Tpoint Tn) (prod (@Tpoint Tn) (prod (@Tpoint Tn) (@Tpoint Tn))) CONCY)) (@fst (@Tpoint Tn) (@Tpoint Tn) (@snd (@Tpoint Tn) (prod (@Tpoint Tn) (@Tpoint Tn)) (@snd (@Tpoint Tn) (prod (@Tpoint Tn) (prod (@Tpoint Tn) (@Tpoint Tn))) CONCY))) (@snd (@Tpoint Tn) (@Tpoint Tn) (@snd (@Tpoint Tn) (prod (@Tpoint Tn) (@Tpoint Tn)) (@snd (@Tpoint Tn) (prod (@Tpoint Tn) (prod (@Tpoint Tn) (@Tpoint Tn))) CONCY))) *)
destruct HConcy as [HConcy1 [HConcy2 [HConcy3 HConcy4]]].
(* Goal: Concyclic_gen A B C D *)
apply concyclic_gen_pseudo_trans with (fst NOT_COL) (fst (snd NOT_COL)) (snd (snd NOT_COL)); try apply concyclic_gen_2341; auto.
Qed.

Global Instance Tarski_is_a_Coinc_theory_for_concy : (Coinc_theory (Build_Arity Tpoint 1) (Build_Coinc_predicates (Build_Arity Tpoint 1) not_col concy)).
Proof.
(* Goal: Coinc_theory (Build_Arity (@Tpoint Tn) (S O)) (Build_Coinc_predicates (Build_Arity (@Tpoint Tn) (S O)) not_col concy) *)
exact (Build_Coinc_theory (Build_Arity Tpoint 1) (Build_Coinc_predicates (Build_Arity Tpoint 1) not_col concy) not_col_perm_1 not_col_perm_2 concy_perm_1 concy_perm_2 concy_bd concy_3).
Qed.

End Tarski_is_a_Coinc_theory_for_concyclic.
