Library GeoCoq.Highschool.concyclic

Require Import GeoCoq.Highschool.circumcenter.

Section Concyclic.

Context `{TE:Tarski_2D_euclidean}.

Definition Concyclic A B C D := Coplanar A B C D ∧ ∃ O, Cong O A O B ∧ Cong O A O C ∧ Cong O A O D.

Lemma concyclic_trans : ∀ 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.
intros.
unfold Concyclic in ×.
decompose [ex and] H0;clear H0.
decompose [ex and] H1;clear H1.
split.
apply all_coplanar.
∃ x.
repeat split;Cong.
assert (x=x0).
assert_diffs.
apply is_circumcenter_uniqueness with A B C;try assumption.
unfold is_circumcenter;split;eCong.
unfold is_circumcenter;split;eCong.
subst.
Cong.
Qed.

Lemma concyclic_perm_1: ∀ A B C D,
  Concyclic A B C D → Concyclic A B D C.
Proof.
intros A B C D H.
destruct H as [H1 [X H2]].
split; try apply all_coplanar; spliter; ∃ X; repeat split; eCong.
Qed.

Lemma concyclic_perm_2 : ∀ A B C D,
  Concyclic A B C D → Concyclic A C B D.
Proof.
intros A B C D H.
destruct H as [H1 [X H2]].
split; try apply all_coplanar; spliter; ∃ X; repeat split; eCong.
Qed.

Lemma concyclic_perm_3 : ∀ A B C D,
  Concyclic A B C D → Concyclic A C D B.
Proof.
intros A B C D H.
destruct H as [H1 [X H2]].
split; try apply all_coplanar; spliter; ∃ X; repeat split; eCong.
Qed.

Lemma concyclic_perm_4 : ∀ A B C D,
  Concyclic A B C D → Concyclic A D B C.
Proof.
intros A B C D H.
destruct H as [H1 [X H2]].
split; try apply all_coplanar; spliter; ∃ X; repeat split; eCong.
Qed.

Lemma concyclic_perm_5 : ∀ A B C D,
  Concyclic A B C D → Concyclic A D C B.
Proof.
intros A B C D H.
destruct H as [H1 [X H2]].
split; try apply all_coplanar; spliter; ∃ X; repeat split; eCong.
Qed.

Lemma concyclic_perm_6 : ∀ A B C D,
  Concyclic A B C D → Concyclic B A C D.
Proof.
intros A B C D H.
destruct H as [H1 [X H2]].
split; try apply all_coplanar; spliter; ∃ X; repeat split; eCong.
Qed.

Lemma concyclic_perm_7 : ∀ A B C D,
  Concyclic A B C D → Concyclic B A D C.
Proof.
intros A B C D H.
destruct H as [H1 [X H2]].
split; try apply all_coplanar; spliter; ∃ X; repeat split; eCong.
Qed.

Lemma concyclic_perm_8 : ∀ A B C D,
  Concyclic A B C D → Concyclic B C A D.
Proof.
intros A B C D H.
destruct H as [H1 [X H2]].
split; try apply all_coplanar; spliter; ∃ X; repeat split; eCong.
Qed.

Lemma concyclic_perm_9 : ∀ A B C D,
  Concyclic A B C D → Concyclic B C D A.
Proof.
intros A B C D H.
destruct H as [H1 [X H2]].
split; try apply all_coplanar; spliter; ∃ X; repeat split; eCong.
Qed.

Lemma concyclic_perm_10 : ∀ A B C D,
  Concyclic A B C D → Concyclic B D A C.
Proof.
intros A B C D H.
destruct H as [H1 [X H2]].
split; try apply all_coplanar; spliter; ∃ X; repeat split; eCong.
Qed.

Lemma concyclic_perm_11 : ∀ A B C D,
  Concyclic A B C D → Concyclic B D C A.
Proof.
intros A B C D H.
destruct H as [H1 [X H2]].
split; try apply all_coplanar; spliter; ∃ X; repeat split; eCong.
Qed.

Lemma concyclic_perm_12 : ∀ A B C D,
  Concyclic A B C D → Concyclic C A B D.
Proof.
intros A B C D H.
destruct H as [H1 [X H2]].
split; try apply all_coplanar; spliter; ∃ X; repeat split; eCong.
Qed.

Lemma concyclic_perm_13 : ∀ A B C D,
  Concyclic A B C D → Concyclic C A D B.
Proof.
intros A B C D H.
destruct H as [H1 [X H2]].
split; try apply all_coplanar; spliter; ∃ X; repeat split; eCong.
Qed.

Lemma concyclic_perm_14 : ∀ A B C D,
  Concyclic A B C D → Concyclic C B A D.
Proof.
intros A B C D H.
destruct H as [H1 [X H2]].
split; try apply all_coplanar; spliter; ∃ X; repeat split; eCong.
Qed.

Lemma concyclic_perm_15 : ∀ A B C D,
  Concyclic A B C D → Concyclic C B D A.
Proof.
intros A B C D H.
destruct H as [H1 [X H2]].
split; try apply all_coplanar; spliter; ∃ X; repeat split; eCong.
Qed.

Lemma concyclic_perm_16 : ∀ A B C D,
  Concyclic A B C D → Concyclic C D A B.
Proof.
intros A B C D H.
destruct H as [H1 [X H2]].
split; try apply all_coplanar; spliter; ∃ X; repeat split; eCong.
Qed.

Lemma concyclic_perm_17 : ∀ A B C D,
  Concyclic A B C D → Concyclic C D B A.
Proof.
intros A B C D H.
destruct H as [H1 [X H2]].
split; try apply all_coplanar; spliter; ∃ X; repeat split; eCong.
Qed.

Lemma concyclic_perm_18 : ∀ A B C D,
  Concyclic A B C D → Concyclic D A B C.
Proof.
intros A B C D H.
destruct H as [H1 [X H2]].
split; try apply all_coplanar; spliter; ∃ X; repeat split; eCong.
Qed.

Lemma concyclic_perm_19 : ∀ A B C D,
  Concyclic A B C D → Concyclic D A C B.
Proof.
intros A B C D H.
destruct H as [H1 [X H2]].
split; try apply all_coplanar; spliter; ∃ X; repeat split; eCong.
Qed.

Lemma concyclic_perm_20 : ∀ A B C D,
  Concyclic A B C D → Concyclic D B A C.
Proof.
intros A B C D H.
destruct H as [H1 [X H2]].
split; try apply all_coplanar; spliter; ∃ X; repeat split; eCong.
Qed.

Lemma concyclic_perm_21 : ∀ A B C D,
  Concyclic A B C D → Concyclic D B C A.
Proof.
intros A B C D H.
destruct H as [H1 [X H2]].
split; try apply all_coplanar; spliter; ∃ X; repeat split; eCong.
Qed.

Lemma concyclic_perm_22 : ∀ A B C D,
  Concyclic A B C D → Concyclic D C A B.
Proof.
intros A B C D H.
destruct H as [H1 [X H2]].
split; try apply all_coplanar; spliter; ∃ X; repeat split; eCong.
Qed.

Lemma concyclic_perm_23 : ∀ A B C D,
  Concyclic A B C D → Concyclic D C B A.
Proof.
intros A B C D H.
destruct H as [H1 [X H2]].
split; try apply all_coplanar; spliter; ∃ X; repeat split; eCong.
Qed.

Lemma concyclic_1123 : ∀ A B C,
 ¬ Col A B C →
 Concyclic A A B C.
Proof.
intros A B C HABC.
unfold Concyclic.
split.
apply coplanar_trivial.
destruct (exists_circumcenter A B C HABC) as [G HG].
∃ G.
apply circumcenter_cong in HG;spliter;repeat split;Cong.
Qed.

End Concyclic.