Require Export GeoCoq.Highschool.circumcenter.

Section Concyclic.

Context `{TE:Tarski_euclidean}.

Definition Concyclic A B C D := Coplanar A B C D /\ exists O, Cong O A O B /\ Cong O A O C /\ Cong O A O D.

Lemma concyclic_aux : forall A B C D, Concyclic A B C D ->
  exists O, Cong O A O B /\ Cong O A O C /\ Cong O A O D /\ Coplanar A B C O.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : Concyclic A B C D), @ex (@Tpoint Tn) (fun O : @Tpoint Tn => and (@Cong Tn O A O B) (and (@Cong Tn O A O C) (and (@Cong Tn O A O D) (@Coplanar Tn A B C O)))) *)
  intros A B C D [HCop [O1]]; spliter.
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => and (@Cong Tn O A O B) (and (@Cong Tn O A O C) (and (@Cong Tn O A O D) (@Coplanar Tn A B C O)))) *)
  destruct (col_dec A B C).
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => and (@Cong Tn O A O B) (and (@Cong Tn O A O C) (and (@Cong Tn O A O D) (@Coplanar Tn A B C O)))) *)
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => and (@Cong Tn O A O B) (and (@Cong Tn O A O C) (and (@Cong Tn O A O D) (@Coplanar Tn A B C O)))) *)
    exists O1; repeat split; Cop.
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => and (@Cong Tn O A O B) (and (@Cong Tn O A O C) (and (@Cong Tn O A O D) (@Coplanar Tn A B C O)))) *)
  destruct (l11_62_existence A B C O1) as [O []].
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => and (@Cong Tn O A O B) (and (@Cong Tn O A O C) (and (@Cong Tn O A O D) (@Coplanar Tn A B C O)))) *)
  exists O.
(* Goal: and (@Cong Tn O A O B) (and (@Cong Tn O A O C) (and (@Cong Tn O A O D) (@Coplanar Tn A B C O))) *)
  repeat split; try apply cong2_per2__cong with O1 O1; Cong; Cop.
Qed.

Lemma concyclic_trans : forall A B C D E,
 ~ Col A B C ->
 Concyclic A B C D  -> Concyclic A B C E -> Concyclic A B D E.
Proof.
(* Goal: forall (A B C D E : @Tpoint Tn) (_ : not (@Col Tn A B C)) (_ : Concyclic A B C D) (_ : Concyclic A B C E), Concyclic A B D E *)
intros.
(* Goal: and (@Coplanar Tn A A B C) (@ex (@Tpoint Tn) (fun O : @Tpoint Tn => and (@Cong Tn O A O A) (and (@Cong Tn O A O B) (@Cong Tn O A O C)))) *)
split.
(* Goal: @Coplanar Tn A B D E *)
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => and (@Cong Tn O A O B) (and (@Cong Tn O A O D) (@Cong Tn O A O E))) *)
unfold Concyclic in *; spliter.
(* Goal: @Coplanar Tn A B D E *)
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => and (@Cong Tn O A O B) (and (@Cong Tn O A O D) (@Cong Tn O A O E))) *)
apply coplanar_trans_1 with C; Col; Cop.
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => and (@Cong Tn O A O B) (and (@Cong Tn O A O D) (@Cong Tn O A O E))) *)
apply concyclic_aux in H0.
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => and (@Cong Tn O A O B) (and (@Cong Tn O A O D) (@Cong Tn O A O E))) *)
apply concyclic_aux in H1.
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => and (@Cong Tn O A O B) (and (@Cong Tn O A O D) (@Cong Tn O A O E))) *)
decompose [ex and] H0;clear H0.
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => and (@Cong Tn O A O B) (and (@Cong Tn O A O D) (@Cong Tn O A O E))) *)
decompose [ex and] H1;clear H1.
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => and (@Cong Tn O A O B) (and (@Cong Tn O A O D) (@Cong Tn O A O E))) *)
exists x.
(* Goal: and (@Cong Tn x A x B) (and (@Cong Tn x A x D) (@Cong Tn x A x E)) *)
repeat split;Cong.
(* Goal: @Cong Tn x A x E *)
assert (x=x0).
(* Goal: @eq (@Tpoint Tn) x x0 *)
(* Goal: @Cong Tn x A x E *)
assert_diffs.
(* Goal: @eq (@Tpoint Tn) x x0 *)
(* Goal: @Cong Tn x A x E *)
apply is_circumcenter_uniqueness with A B C;try assumption.
(* Goal: @is_circumcenter Tn x0 A B C *)
(* Goal: @Cong Tn x A x E *)
unfold is_circumcenter;repeat split;[eCong..|Cop].
(* Goal: @is_circumcenter Tn x0 A B C *)
(* Goal: @Cong Tn x A x E *)
unfold is_circumcenter;repeat split;[eCong..|Cop].
(* Goal: @Cong Tn x A x E *)
subst.
(* Goal: @Cong Tn x0 A x0 E *)
Cong.
Qed.

Lemma concyclic_perm_1: forall A B C D,
  Concyclic A B C D -> Concyclic A B D C.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : Concyclic A B C D), Concyclic D C B A *)
intros A B C D H.
(* Goal: Concyclic D C B A *)
destruct H as [H1 [X H2]].
(* Goal: @Cong Tn x0 A x0 E *)
split; [Cop|spliter; exists X; repeat split; eCong..].
Qed.

Lemma concyclic_perm_2 : forall A B C D,
  Concyclic A B C D -> Concyclic A C B D.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : Concyclic A B C D), Concyclic D C B A *)
intros A B C D H.
(* Goal: Concyclic D C B A *)
destruct H as [H1 [X H2]].
(* Goal: @Cong Tn x0 A x0 E *)
split; [Cop|spliter; exists X; repeat split; eCong..].
Qed.

Lemma concyclic_perm_3 : forall A B C D,
  Concyclic A B C D -> Concyclic A C D B.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : Concyclic A B C D), Concyclic D C B A *)
intros A B C D H.
(* Goal: Concyclic D C B A *)
destruct H as [H1 [X H2]].
(* Goal: @Cong Tn x0 A x0 E *)
split; [Cop|spliter; exists X; repeat split; eCong..].
Qed.

Lemma concyclic_perm_4 : forall A B C D,
  Concyclic A B C D -> Concyclic A D B C.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : Concyclic A B C D), Concyclic D C B A *)
intros A B C D H.
(* Goal: Concyclic D C B A *)
destruct H as [H1 [X H2]].
(* Goal: @Cong Tn x0 A x0 E *)
split; [Cop|spliter; exists X; repeat split; eCong..].
Qed.

Lemma concyclic_perm_5 : forall A B C D,
  Concyclic A B C D -> Concyclic A D C B.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : Concyclic A B C D), Concyclic D C B A *)
intros A B C D H.
(* Goal: Concyclic D C B A *)
destruct H as [H1 [X H2]].
(* Goal: @Cong Tn x0 A x0 E *)
split; [Cop|spliter; exists X; repeat split; eCong..].
Qed.

Lemma concyclic_perm_6 : forall A B C D,
  Concyclic A B C D -> Concyclic B A C D.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : Concyclic A B C D), Concyclic D C B A *)
intros A B C D H.
(* Goal: Concyclic D C B A *)
destruct H as [H1 [X H2]].
(* Goal: @Cong Tn x0 A x0 E *)
split; [Cop|spliter; exists X; repeat split; eCong..].
Qed.

Lemma concyclic_perm_7 : forall A B C D,
  Concyclic A B C D -> Concyclic B A D C.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : Concyclic A B C D), Concyclic D C B A *)
intros A B C D H.
(* Goal: Concyclic D C B A *)
destruct H as [H1 [X H2]].
(* Goal: @Cong Tn x0 A x0 E *)
split; [Cop|spliter; exists X; repeat split; eCong..].
Qed.

Lemma concyclic_perm_8 : forall A B C D,
  Concyclic A B C D -> Concyclic B C A D.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : Concyclic A B C D), Concyclic D C B A *)
intros A B C D H.
(* Goal: Concyclic D C B A *)
destruct H as [H1 [X H2]].
(* Goal: @Cong Tn x0 A x0 E *)
split; [Cop|spliter; exists X; repeat split; eCong..].
Qed.

Lemma concyclic_perm_9 : forall A B C D,
  Concyclic A B C D -> Concyclic B C D A.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : Concyclic A B C D), Concyclic D C B A *)
intros A B C D H.
(* Goal: Concyclic D C B A *)
destruct H as [H1 [X H2]].
(* Goal: @Cong Tn x0 A x0 E *)
split; [Cop|spliter; exists X; repeat split; eCong..].
Qed.

Lemma concyclic_perm_10 : forall A B C D,
  Concyclic A B C D -> Concyclic B D A C.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : Concyclic A B C D), Concyclic D C B A *)
intros A B C D H.
(* Goal: Concyclic D C B A *)
destruct H as [H1 [X H2]].
(* Goal: @Cong Tn x0 A x0 E *)
split; [Cop|spliter; exists X; repeat split; eCong..].
Qed.

Lemma concyclic_perm_11 : forall A B C D,
  Concyclic A B C D -> Concyclic B D C A.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : Concyclic A B C D), Concyclic D C B A *)
intros A B C D H.
(* Goal: Concyclic D C B A *)
destruct H as [H1 [X H2]].
(* Goal: @Cong Tn x0 A x0 E *)
split; [Cop|spliter; exists X; repeat split; eCong..].
Qed.

Lemma concyclic_perm_12 : forall A B C D,
  Concyclic A B C D -> Concyclic C A B D.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : Concyclic A B C D), Concyclic D C B A *)
intros A B C D H.
(* Goal: Concyclic D C B A *)
destruct H as [H1 [X H2]].
(* Goal: @Cong Tn x0 A x0 E *)
split; [Cop|spliter; exists X; repeat split; eCong..].
Qed.

Lemma concyclic_perm_13 : forall A B C D,
  Concyclic A B C D -> Concyclic C A D B.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : Concyclic A B C D), Concyclic D C B A *)
intros A B C D H.
(* Goal: Concyclic D C B A *)
destruct H as [H1 [X H2]].
(* Goal: @Cong Tn x0 A x0 E *)
split; [Cop|spliter; exists X; repeat split; eCong..].
Qed.

Lemma concyclic_perm_14 : forall A B C D,
  Concyclic A B C D -> Concyclic C B A D.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : Concyclic A B C D), Concyclic D C B A *)
intros A B C D H.
(* Goal: Concyclic D C B A *)
destruct H as [H1 [X H2]].
(* Goal: @Cong Tn x0 A x0 E *)
split; [Cop|spliter; exists X; repeat split; eCong..].
Qed.

Lemma concyclic_perm_15 : forall A B C D,
  Concyclic A B C D -> Concyclic C B D A.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : Concyclic A B C D), Concyclic D C B A *)
intros A B C D H.
(* Goal: Concyclic D C B A *)
destruct H as [H1 [X H2]].
(* Goal: @Cong Tn x0 A x0 E *)
split; [Cop|spliter; exists X; repeat split; eCong..].
Qed.

Lemma concyclic_perm_16 : forall A B C D,
  Concyclic A B C D -> Concyclic C D A B.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : Concyclic A B C D), Concyclic D C B A *)
intros A B C D H.
(* Goal: Concyclic D C B A *)
destruct H as [H1 [X H2]].
(* Goal: @Cong Tn x0 A x0 E *)
split; [Cop|spliter; exists X; repeat split; eCong..].
Qed.

Lemma concyclic_perm_17 : forall A B C D,
  Concyclic A B C D -> Concyclic C D B A.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : Concyclic A B C D), Concyclic D C B A *)
intros A B C D H.
(* Goal: Concyclic D C B A *)
destruct H as [H1 [X H2]].
(* Goal: @Cong Tn x0 A x0 E *)
split; [Cop|spliter; exists X; repeat split; eCong..].
Qed.

Lemma concyclic_perm_18 : forall A B C D,
  Concyclic A B C D -> Concyclic D A B C.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : Concyclic A B C D), Concyclic D C B A *)
intros A B C D H.
(* Goal: Concyclic D C B A *)
destruct H as [H1 [X H2]].
(* Goal: @Cong Tn x0 A x0 E *)
split; [Cop|spliter; exists X; repeat split; eCong..].
Qed.

Lemma concyclic_perm_19 : forall A B C D,
  Concyclic A B C D -> Concyclic D A C B.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : Concyclic A B C D), Concyclic D C B A *)
intros A B C D H.
(* Goal: Concyclic D C B A *)
destruct H as [H1 [X H2]].
(* Goal: @Cong Tn x0 A x0 E *)
split; [Cop|spliter; exists X; repeat split; eCong..].
Qed.

Lemma concyclic_perm_20 : forall A B C D,
  Concyclic A B C D -> Concyclic D B A C.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : Concyclic A B C D), Concyclic D C B A *)
intros A B C D H.
(* Goal: Concyclic D C B A *)
destruct H as [H1 [X H2]].
(* Goal: @Cong Tn x0 A x0 E *)
split; [Cop|spliter; exists X; repeat split; eCong..].
Qed.

Lemma concyclic_perm_21 : forall A B C D,
  Concyclic A B C D -> Concyclic D B C A.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : Concyclic A B C D), Concyclic D C B A *)
intros A B C D H.
(* Goal: Concyclic D C B A *)
destruct H as [H1 [X H2]].
(* Goal: @Cong Tn x0 A x0 E *)
split; [Cop|spliter; exists X; repeat split; eCong..].
Qed.

Lemma concyclic_perm_22 : forall A B C D,
  Concyclic A B C D -> Concyclic D C A B.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : Concyclic A B C D), Concyclic D C B A *)
intros A B C D H.
(* Goal: Concyclic D C B A *)
destruct H as [H1 [X H2]].
(* Goal: @Cong Tn x0 A x0 E *)
split; [Cop|spliter; exists X; repeat split; eCong..].
Qed.

Lemma concyclic_perm_23 : forall A B C D,
  Concyclic A B C D -> Concyclic D C B A.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : Concyclic A B C D), Concyclic D C B A *)
intros A B C D H.
(* Goal: Concyclic D C B A *)
destruct H as [H1 [X H2]].
(* Goal: @Cong Tn x0 A x0 E *)
split; [Cop|spliter; exists X; repeat split; eCong..].
Qed.

Lemma concyclic_1123 : forall A B C,
 ~ Col A B C ->
 Concyclic A A B C.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)), Concyclic A A B C *)
intros A B C HABC.
(* Goal: Concyclic A A B C *)
unfold Concyclic.
(* Goal: and (@Coplanar Tn A A B C) (@ex (@Tpoint Tn) (fun O : @Tpoint Tn => and (@Cong Tn O A O A) (and (@Cong Tn O A O B) (@Cong Tn O A O C)))) *)
split.
(* Goal: @Coplanar Tn A A B C *)
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => and (@Cong Tn O A O A) (and (@Cong Tn O A O B) (@Cong Tn O A O C))) *)
apply coplanar_trivial.
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => and (@Cong Tn O A O A) (and (@Cong Tn O A O B) (@Cong Tn O A O C))) *)
destruct (exists_circumcenter A B C HABC) as [G HG].
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => and (@Cong Tn O A O A) (and (@Cong Tn O A O B) (@Cong Tn O A O C))) *)
exists G.
(* Goal: and (@Cong Tn x A x B) (and (@Cong Tn x A x D) (@Cong Tn x A x E)) *)
apply circumcenter_cong in HG;spliter;repeat split;Cong.
Qed.

End Concyclic.
