Require Export GeoCoq.Highschool.bisector.
Require Export GeoCoq.Tarski_dev.Ch13_1.

Section InCenter.

Context `{TE:Tarski_euclidean}.


Definition is_incenter I A B C :=
 ~ Col A B C /\ CongA B A I I A C /\ CongA A B I I B C /\ CongA A C I I C B.

(** Proof of the existence of the incenter of a triangle. *)

Lemma incenter_exists : forall A B C, ~ Col A B C -> exists I, is_incenter I A B C.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)), @ex (@Tpoint Tn) (fun I : @Tpoint Tn => is_incenter I A B C) *)
intros A B C HNCOL.
(*----construction---*)
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => is_incenter I A B C) *)
destruct (bisector_existence A B C) as [IB HCONA].
(* Goal: not (@Col Tn C A B) *)
(* Goal: @InAngle Tn X C A B *)
(* Goal: @OS Tn C B A X *)
(* Goal: @Col Tn C HB A *)
(* Goal: @Col Tn C HA B *)
(* Goal: @Perp Tn C B X HA *)
assert_diffs;auto.
(* Goal: not (@Col Tn C A B) *)
(* Goal: @InAngle Tn X C A B *)
(* Goal: @OS Tn C B A X *)
(* Goal: @Col Tn C HB A *)
(* Goal: @Col Tn C HA B *)
(* Goal: @Perp Tn C B X HA *)
assert_diffs;auto.
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => is_incenter I A B C) *)
destruct (bisector_existence B A C) as [IA HCONB].
(* Goal: not (@Col Tn C A B) *)
(* Goal: @InAngle Tn X C A B *)
(* Goal: @OS Tn C B A X *)
(* Goal: @Col Tn C HB A *)
(* Goal: @Col Tn C HA B *)
(* Goal: @Perp Tn C B X HA *)
assert_diffs;auto.
(* Goal: not (@Col Tn C A B) *)
(* Goal: @InAngle Tn X C A B *)
(* Goal: @OS Tn C B A X *)
(* Goal: @Col Tn C HB A *)
(* Goal: @Col Tn C HA B *)
(* Goal: @Perp Tn C B X HA *)
assert_diffs;auto.
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => is_incenter I A B C) *)
destruct HCONA as [HBINANGLE HCONGAA].
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => is_incenter I A B C) *)
destruct HCONB as [HAINANGLE HCONGBB].
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => is_incenter I A B C) *)
unfold InAngle in *.
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => is_incenter I A B C) *)
destruct HBINANGLE as [HBAB [HBCB [HBIBB HBEXI]]].
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => is_incenter I A B C) *)
destruct HAINANGLE as [HABA [HACA [HAIAA HAEXI]]].
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => is_incenter I A B C) *)
destruct HAEXI as [XA HXA].
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => is_incenter I A B C) *)
destruct HBEXI as [XB HXB].
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => is_incenter I A B C) *)
assert (HXEXISTS : exists X : Tpoint, Bet XB X B /\ Bet XA X A).
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn XB X B) (@Bet Tn XA X A)) *)
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => is_incenter I A B C) *)
apply (inner_pasch A B C XB XA).
(* Goal: @Bet Tn A XB C *)
(* Goal: @Bet Tn B XA C *)
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => is_incenter I A B C) *)
destruct HXB; auto.
(* Goal: @Bet Tn B XA C *)
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => is_incenter I A B C) *)
destruct HXA; auto.
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => is_incenter I A B C) *)
destruct HXEXISTS as [X HX].
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => is_incenter I A B C) *)
destruct HXB as [HXBBET HXBO].
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => is_incenter I A B C) *)
destruct HXA as [HXABET HXAO].
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => is_incenter I A B C) *)
destruct HX as [HXBET1 HXBET2].
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => is_incenter I A B C) *)
destruct HXAO as [HXAEQ | HXAOUT].
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => is_incenter I A B C) *)
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => is_incenter I A B C) *)
subst.
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => is_incenter I A B C) *)
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => is_incenter I A B C) *)
elim HNCOL.
(* Goal: @Col Tn A B C *)
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => is_incenter I A B C) *)
assert_diffs;ColR.
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => is_incenter I A B C) *)
destruct HXBO as [HXBEQ | HXBOUT].
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => is_incenter I A B C) *)
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => is_incenter I A B C) *)
subst.
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => is_incenter I A B C) *)
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => is_incenter I A B C) *)
elim HNCOL.
(* Goal: @Col Tn A B C *)
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => is_incenter I A B C) *)
assert_diffs;ColR.
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => is_incenter I A B C) *)
assert (XA <> B) by (intro;subst;assert (Col B A C) by (col_with_conga);Col).
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => is_incenter I A B C) *)
assert (XB <> A) by (intro;subst;elim HNCOL;col_with_conga).
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => is_incenter I A B C) *)
assert (X <> A) by (intro;subst;elim HNCOL;col_with_conga).
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => is_incenter I A B C) *)
assert (X <> B) by (intro;subst;assert (Col B A C) by (col_with_conga);elim HNCOL;Col).
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => is_incenter I A B C) *)
assert (~ Col A B X) by (intro;elim HNCOL;col_with_conga).
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => is_incenter I A B C) *)
assert (~ Col A C X) by (intro;assert (Col C A B) by (col_with_conga);elim HNCOL;Col).
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => is_incenter I A B C) *)
assert (~ Col B C X) by (intro;assert (Col C B A) by (col_with_conga);elim HNCOL;Col).
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => is_incenter I A B C) *)
destruct (l8_18_existence A B X) as [HC [HCC1 HCC2]];auto.
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => is_incenter I A B C) *)
destruct (l8_18_existence A C X) as [HB [HBC1 HBC2]];auto.
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => is_incenter I A B C) *)
destruct (l8_18_existence B C X) as [HA [HAC1 HAC2]];auto.
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => is_incenter I A B C) *)
exists X.
(* Goal: or (is_incenter I A B C) (not (is_incenter I A B C)) *)
unfold is_incenter.
(* Goal: and (not (@Col Tn B A C)) (and (@CongA Tn A B I I B C) (and (@CongA Tn B A I I A C) (@CongA Tn B C I I C A))) *)
split.
(* Goal: not (@Col Tn A B C) *)
(* Goal: and (@CongA Tn B A X X A C) (and (@CongA Tn A B X X B C) (@CongA Tn A C X X C B)) *)
assumption.
(*-prove some conclusions which will be required later for many times.-*)
assert (Out A IA X) by (assert (Bet A X XA) by (Between); 
assert (Out A X XA) by (apply (bet_out A X XA);auto;assert_diffs;auto); 
apply (l6_6 A X IA);auto;apply (l6_7 A X XA IA);auto).
assert (Out B IB X) by (assert (Bet B X XB) by (Between);
assert (Out B X XB) by (apply (bet_out B X XB);auto;assert_diffs;auto);
apply (l6_6 B X IB);auto;apply (l6_7 B X XB IB);auto).
(* Goal: and (@CongA Tn B A X X A C) (and (@CongA Tn A B X X B C) (@CongA Tn A C X X C B)) *)
assert (CongA B A X X A C).
(* Goal: @CongA Tn A C X X C B *)
(* Goal: and (@CongA Tn B A X X A C) (and (@CongA Tn A B X X B C) (@CongA Tn A C X X C B)) *)
{ apply (out_conga B A IA IA A C B X X C);auto. 
(* Goal: @Out Tn A B B *)
(* Goal: @Out Tn A C C *)
  apply (out_trivial A B);auto.
(* Goal: @Out Tn A C C *)
  apply (out_trivial A C);auto.
}
(* Goal: and (@CongA Tn B A X X A C) (and (@CongA Tn A B X X B C) (@CongA Tn A C X X C B)) *)
assert (CongA A B X X B C).
(* Goal: @CongA Tn A C X X C B *)
(* Goal: and (@CongA Tn B A X X A C) (and (@CongA Tn A B X X B C) (@CongA Tn A C X X C B)) *)
{ apply (out_conga A B IB IB B C A X X C);auto.
(* Goal: @Out Tn B A A *)
(* Goal: @Out Tn B C C *)
 apply (out_trivial B A);auto.
(* Goal: @Out Tn B C C *)
 apply (out_trivial B C);auto.
}
(* Goal: and (@CongA Tn B A X X A C) (and (@CongA Tn A B X X B C) (@CongA Tn A C X X C B)) *)
assert (Coplanar C A B X) by (exists XB; left; split; Col).
(* Goal: and (@CongA Tn B A X X A C) (and (@CongA Tn A B X X B C) (@CongA Tn A C X X C B)) *)
assert (Cong X HB X HC) by (apply (bisector_perp_equality C A B X HB HC);Col;Perp;CongA).
(* Goal: and (@CongA Tn B A X X A C) (and (@CongA Tn A B X X B C) (@CongA Tn A C X X C B)) *)
assert (Cong X HC X HA) by (apply (bisector_perp_equality A B C X HC HA);Col;Cop).
(* Goal: and (@CongA Tn B A X X A C) (and (@CongA Tn A B X X B C) (@CongA Tn A C X X C B)) *)
assert (Cong X HB X HA) by (apply (cong_transitivity X HB X HC X HA);auto).
(* Goal: and (@CongA Tn B A X X A C) (and (@CongA Tn A B X X B C) (@CongA Tn A C X X C B)) *)
assert (CongA A C X X C B).
(* Goal: @CongA Tn A C X X C B *)
(* Goal: and (@CongA Tn B A X X A C) (and (@CongA Tn A B X X B C) (@CongA Tn A C X X C B)) *)
{ 
(* Goal: @CongA Tn A C X X C B *)
 apply (perp_equality_bisector A C B X HB HA);auto.
(* Goal: not (@Col Tn C B A) *)
(* Goal: @InAngle Tn X C B A *)
(* Goal: @Col Tn C HB A *)
(* Goal: @Col Tn C HA B *)
(* Goal: @Perp Tn C B X HA *)
 intro;elim HNCOL;Col.
(* Goal: @InAngle Tn X A C B *)
(* Goal: @Col Tn C HB A *)
(* Goal: @Col Tn C HA B *)
(* Goal: @Perp Tn C B X HA *)
 assert (InAngle X A B C).
(* Goal: @InAngle Tn X B A C *)
(* Goal: @InAngle Tn X A C B *)
(* Goal: @Col Tn C HB A *)
(* Goal: @Col Tn C HA B *)
(* Goal: @Perp Tn C B X HA *)
 unfold InAngle.
(* Goal: and (not (@Col Tn B A C)) (and (@CongA Tn A B I I B C) (and (@CongA Tn B A I I A C) (@CongA Tn B C I I C A))) *)
 repeat split.
(* Goal: not (@Col Tn C A B) *)
(* Goal: @InAngle Tn X C A B *)
(* Goal: @OS Tn C B A X *)
(* Goal: @Col Tn C HB A *)
(* Goal: @Col Tn C HA B *)
(* Goal: @Perp Tn C B X HA *)
 assert_diffs;auto.
(* Goal: not (@Col Tn C A B) *)
(* Goal: @InAngle Tn X C A B *)
(* Goal: @OS Tn C B A X *)
(* Goal: @Col Tn C HB A *)
(* Goal: @Col Tn C HA B *)
(* Goal: @Perp Tn C B X HA *)
 assert_diffs;auto.
(* Goal: not (@Col Tn C A B) *)
(* Goal: @InAngle Tn X C A B *)
(* Goal: @OS Tn C B A X *)
(* Goal: @Col Tn C HB A *)
(* Goal: @Col Tn C HA B *)
(* Goal: @Perp Tn C B X HA *)
 assert_diffs;auto.
(* Goal: @ex (@Tpoint Tn) (fun X0 : @Tpoint Tn => and (@Bet Tn A X0 C) (or (@eq (@Tpoint Tn) X0 B) (@Out Tn B X0 X))) *)
(* Goal: @InAngle Tn X A C B *)
(* Goal: @Col Tn C HB A *)
(* Goal: @Col Tn C HA B *)
(* Goal: @Perp Tn C B X HA *)
 exists XB.
(* Goal: and (@CongA Tn B A X X A C) (and (@CongA Tn A B X X B C) (@CongA Tn A C X X C B)) *)
 split;auto.
(* Goal: or (is_incenter I A B C) (not (is_incenter I A B C)) *)
(* Goal: or (is_incenter I A B C) (not (is_incenter I A B C)) *)
 right.
(* Goal: @Out Tn B XB X *)
(* Goal: @InAngle Tn X A C B *)
(* Goal: @Col Tn C HB A *)
(* Goal: @Col Tn C HA B *)
(* Goal: @Perp Tn C B X HA *)
 apply (l6_6 B X XB);auto.
(* Goal: @Out Tn B X XB *)
(* Goal: @InAngle Tn X A C B *)
(* Goal: @Col Tn C HB A *)
(* Goal: @Col Tn C HA B *)
(* Goal: @Perp Tn C B X HA *)
 apply (bet_out B X XB);auto.
(* Goal: not (@Col Tn C A B) *)
(* Goal: @InAngle Tn X C A B *)
(* Goal: @OS Tn C B A X *)
(* Goal: @Col Tn C HB A *)
(* Goal: @Col Tn C HA B *)
(* Goal: @Perp Tn C B X HA *)
 assert_diffs;auto.
(* Goal: @Bet Tn A X XA *)
(* Goal: @InAngle Tn X A C B *)
(* Goal: @Col Tn C HB A *)
(* Goal: @Col Tn C HA B *)
(* Goal: @Perp Tn C B X HA *)
 Between.
(* Goal: @InAngle Tn X A C B *)
(* Goal: @Col Tn C HB A *)
(* Goal: @Col Tn C HA B *)
(* Goal: @Perp Tn C B X HA *)
 assert (InAngle X B A C).
(* Goal: @InAngle Tn X B A C *)
(* Goal: @InAngle Tn X A C B *)
(* Goal: @Col Tn C HB A *)
(* Goal: @Col Tn C HA B *)
(* Goal: @Perp Tn C B X HA *)
 unfold InAngle.
(* Goal: and (not (@Col Tn B A C)) (and (@CongA Tn A B I I B C) (and (@CongA Tn B A I I A C) (@CongA Tn B C I I C A))) *)
 repeat split.
(* Goal: not (@Col Tn C A B) *)
(* Goal: @InAngle Tn X C A B *)
(* Goal: @OS Tn C B A X *)
(* Goal: @Col Tn C HB A *)
(* Goal: @Col Tn C HA B *)
(* Goal: @Perp Tn C B X HA *)
 assert_diffs;auto.
(* Goal: not (@Col Tn C A B) *)
(* Goal: @InAngle Tn X C A B *)
(* Goal: @OS Tn C B A X *)
(* Goal: @Col Tn C HB A *)
(* Goal: @Col Tn C HA B *)
(* Goal: @Perp Tn C B X HA *)
 assert_diffs;auto.
(* Goal: not (@Col Tn C A B) *)
(* Goal: @InAngle Tn X C A B *)
(* Goal: @OS Tn C B A X *)
(* Goal: @Col Tn C HB A *)
(* Goal: @Col Tn C HA B *)
(* Goal: @Perp Tn C B X HA *)
 assert_diffs;auto.
(* Goal: @ex (@Tpoint Tn) (fun X0 : @Tpoint Tn => and (@Bet Tn B X0 C) (or (@eq (@Tpoint Tn) X0 A) (@Out Tn A X0 X))) *)
(* Goal: @InAngle Tn X A C B *)
(* Goal: @Col Tn C HB A *)
(* Goal: @Col Tn C HA B *)
(* Goal: @Perp Tn C B X HA *)
 exists XA.
(* Goal: and (@CongA Tn B A X X A C) (and (@CongA Tn A B X X B C) (@CongA Tn A C X X C B)) *)
 split;auto.
(* Goal: or (is_incenter I A B C) (not (is_incenter I A B C)) *)
(* Goal: or (is_incenter I A B C) (not (is_incenter I A B C)) *)
 right.
(* Goal: @Out Tn A XA X *)
(* Goal: @InAngle Tn X A C B *)
(* Goal: @Col Tn C HB A *)
(* Goal: @Col Tn C HA B *)
(* Goal: @Perp Tn C B X HA *)
 apply (l6_6 A X XA);auto.
(* Goal: @Out Tn A X XA *)
(* Goal: @InAngle Tn X A C B *)
(* Goal: @Col Tn C HB A *)
(* Goal: @Col Tn C HA B *)
(* Goal: @Perp Tn C B X HA *)
 apply (bet_out A X XA);auto.
(* Goal: not (@Col Tn C A B) *)
(* Goal: @InAngle Tn X C A B *)
(* Goal: @OS Tn C B A X *)
(* Goal: @Col Tn C HB A *)
(* Goal: @Col Tn C HA B *)
(* Goal: @Perp Tn C B X HA *)
 assert_diffs;auto.
(* Goal: @Bet Tn A X XA *)
(* Goal: @InAngle Tn X A C B *)
(* Goal: @Col Tn C HB A *)
(* Goal: @Col Tn C HA B *)
(* Goal: @Perp Tn C B X HA *)
 Between.
(* Goal: @InAngle Tn X A C B *)
(* Goal: @Col Tn C HB A *)
(* Goal: @Col Tn C HA B *)
(* Goal: @Perp Tn C B X HA *)
 apply (os2__inangle A C B X);auto.
(* Goal: @OS Tn C A B X *)
(* Goal: @OS Tn C B A X *)
(* Goal: @Col Tn C HB A *)
(* Goal: @Col Tn C HA B *)
(* Goal: @Perp Tn C B X HA *)
 apply (one_side_symmetry C A X B);auto.
(* Goal: @OS Tn C A X B *)
(* Goal: @OS Tn C B A X *)
(* Goal: @Col Tn C HB A *)
(* Goal: @Col Tn C HA B *)
(* Goal: @Perp Tn C B X HA *)
 apply (in_angle_one_side C A B X);auto.
(* Goal: not (@Col Tn C A B) *)
(* Goal: @InAngle Tn X C A B *)
(* Goal: @OS Tn C B A X *)
(* Goal: @Col Tn C HB A *)
(* Goal: @Col Tn C HA B *)
(* Goal: @Perp Tn C B X HA *)
 assert_diffs;auto.
(* Goal: not (@Col Tn C B A) *)
(* Goal: @InAngle Tn X C B A *)
(* Goal: @Col Tn C HB A *)
(* Goal: @Col Tn C HA B *)
(* Goal: @Perp Tn C B X HA *)
 intro; elim HNCOL; Col.
(* Goal: @InAngle Tn X C A B *)
(* Goal: @OS Tn C B A X *)
(* Goal: @Col Tn C HB A *)
(* Goal: @Col Tn C HA B *)
(* Goal: @Perp Tn C B X HA *)
 apply (l11_24 X B A C);auto.
(* Goal: @OS Tn C B A X *)
(* Goal: @Col Tn C HB A *)
(* Goal: @Col Tn C HA B *)
(* Goal: @Perp Tn C B X HA *)
 apply (one_side_symmetry C B X A);auto.
(* Goal: @OS Tn C B X A *)
(* Goal: @Col Tn C HB A *)
(* Goal: @Col Tn C HA B *)
(* Goal: @Perp Tn C B X HA *)
 apply (in_angle_one_side C B A X);auto.
(* Goal: not (@Col Tn C B A) *)
(* Goal: @InAngle Tn X C B A *)
(* Goal: @Col Tn C HB A *)
(* Goal: @Col Tn C HA B *)
(* Goal: @Perp Tn C B X HA *)
 intro; elim HNCOL; Col.
(* Goal: @InAngle Tn X C B A *)
(* Goal: @Col Tn C HB A *)
(* Goal: @Col Tn C HA B *)
(* Goal: @Perp Tn C B X HA *)
 apply (l11_24 X A B C);auto.
(* Goal: @Col Tn C HA B *)
(* Goal: @Perp Tn C B X HA *)
 Col.
(* Goal: @Col Tn C HA B *)
(* Goal: @Perp Tn C B X HA *)
 Col.
(* Goal: @Perp Tn C B X HA *)
 Perp.
}
(* Goal: and (@CongA Tn B A X X A C) (and (@CongA Tn A B X X B C) (@CongA Tn A C X X C B)) *)
split;auto.
Qed.

Lemma incenter_permut132 : forall A B C I, is_incenter I A B C -> is_incenter I A C B.
Proof.
(* Goal: forall (A B C I : @Tpoint Tn) (_ : is_incenter I A B C), is_incenter I C B A *)
intros A B C I HIABC.
(* Goal: is_incenter I B A C *)
unfold is_incenter in *.
(* Goal: and (not (@Col Tn B A C)) (and (@CongA Tn A B I I B C) (and (@CongA Tn B A I I A C) (@CongA Tn B C I I C A))) *)
destruct HIABC as [HNCOL [HCONGAA [HCONGAB HCONGAC]]].
(* Goal: and (not (@Col Tn B A C)) (and (@CongA Tn A B I I B C) (and (@CongA Tn B A I I A C) (@CongA Tn B C I I C A))) *)
split.
(* Goal: @Col Tn C HA B *)
(* Goal: @Perp Tn C B X HA *)
intro;Col.
(* Goal: and (@CongA Tn A B I I B C) (and (@CongA Tn B A I I A C) (@CongA Tn B C I I C A)) *)
split;CongA.
Qed.

Lemma incenter_permut213 : forall A B C I, is_incenter I A B C -> is_incenter I B A C.
Proof.
(* Goal: forall (A B C I : @Tpoint Tn) (_ : is_incenter I A B C), is_incenter I C B A *)
intros A B C I HIABC.
(* Goal: is_incenter I B A C *)
unfold is_incenter in *.
(* Goal: and (not (@Col Tn B A C)) (and (@CongA Tn A B I I B C) (and (@CongA Tn B A I I A C) (@CongA Tn B C I I C A))) *)
destruct HIABC as [HNCOL [HCONGAA [HCONGAB HCONGAC]]].
(* Goal: and (not (@Col Tn B A C)) (and (@CongA Tn A B I I B C) (and (@CongA Tn B A I I A C) (@CongA Tn B C I I C A))) *)
split.
(* Goal: @Col Tn C HA B *)
(* Goal: @Perp Tn C B X HA *)
intro;Col.
(* Goal: and (@CongA Tn A B I I B C) (and (@CongA Tn B A I I A C) (@CongA Tn B C I I C A)) *)
split;CongA.
Qed.

Lemma incenter_permut231 : forall A B C I, is_incenter I A B C -> is_incenter I B C A.
Proof.
(* Goal: forall (A B C I : @Tpoint Tn) (_ : is_incenter I A B C), is_incenter I C B A *)
intros A B C I HIABC.
(* Goal: is_incenter I B C A *)
apply (incenter_permut132 B A C I);auto.
(* Goal: is_incenter I B A C *)
apply (incenter_permut213 A B C I);auto.
Qed.

Lemma incenter_permut312 : forall A B C I, is_incenter I A B C -> is_incenter I C A B.
Proof.
(* Goal: forall (A B C I : @Tpoint Tn) (_ : is_incenter I A B C), is_incenter I C B A *)
intros A B C I HIABC.
(* Goal: is_incenter I C A B *)
apply (incenter_permut213 A C B I);auto.
(* Goal: is_incenter I A C B *)
apply (incenter_permut132 A B C I);auto.
Qed.

Lemma incenter_permut321 : forall A B C I, is_incenter I A B C -> is_incenter I C B A.
Proof.
(* Goal: forall (A B C I : @Tpoint Tn) (_ : is_incenter I A B C), is_incenter I C B A *)
intros A B C I HIABC.
(* Goal: is_incenter I C B A *)
apply (incenter_permut312 B A C I);auto.
(* Goal: is_incenter I B A C *)
apply (incenter_permut213 A B C);auto.
Qed.

Lemma incenter_dec : forall A B C I, is_incenter I A B C \/ ~ is_incenter I A B C.
Proof.
(* Goal: forall A B C I : @Tpoint Tn, or (is_incenter I A B C) (not (is_incenter I A B C)) *)
intros A B C I.
(* Goal: or (is_incenter I A B C) (not (is_incenter I A B C)) *)
destruct (col_dec A B C) as [HCOL | HNCOL].
(* Goal: or (is_incenter I A B C) (not (is_incenter I A B C)) *)
(* Goal: or (is_incenter I A B C) (not (is_incenter I A B C)) *)
right.
(* Goal: or (is_incenter I A B C) (not (is_incenter I A B C)) *)
unfold is_incenter.
(* Goal: not (and (not (@Col Tn A B C)) (and (@CongA Tn B A I I A C) (and (@CongA Tn A B I I B C) (@CongA Tn A C I I C B)))) *)
(* Goal: or (is_incenter I A B C) (not (is_incenter I A B C)) *)
intro HCOLIN.
(* Goal: False *)
(* Goal: or (is_incenter I A B C) (not (is_incenter I A B C)) *)
destruct HCOLIN as [HNCOL [HCONGAA [HCONGAB HCONGAC]]].
(* Goal: False *)
(* Goal: or (is_incenter I A B C) (not (is_incenter I A B C)) *)
elim HNCOL;auto.
(* Goal: or (is_incenter I A B C) (not (is_incenter I A B C)) *)
unfold is_incenter.
(* Goal: or (and (not (@Col Tn A B C)) (and (@CongA Tn B A I I A C) (and (@CongA Tn A B I I B C) (@CongA Tn A C I I C B)))) (not (and (not (@Col Tn A B C)) (and (@CongA Tn B A I I A C) (and (@CongA Tn A B I I B C) (@CongA Tn A C I I C B))))) *)
destruct (conga_dec B A I I A C) as [HAC | HANC].
(* Goal: or (and (not (@Col Tn A B C)) (and (@CongA Tn B A I I A C) (and (@CongA Tn A B I I B C) (@CongA Tn A C I I C B)))) (not (and (not (@Col Tn A B C)) (and (@CongA Tn B A I I A C) (and (@CongA Tn A B I I B C) (@CongA Tn A C I I C B))))) *)
(* Goal: or (and (not (@Col Tn A B C)) (and (@CongA Tn B A I I A C) (and (@CongA Tn A B I I B C) (@CongA Tn A C I I C B)))) (not (and (not (@Col Tn A B C)) (and (@CongA Tn B A I I A C) (and (@CongA Tn A B I I B C) (@CongA Tn A C I I C B))))) *)
destruct (conga_dec A B I I B C) as [HBC | HBNC].
(* Goal: or (and (not (@Col Tn A B C)) (and (@CongA Tn B A I I A C) (and (@CongA Tn A B I I B C) (@CongA Tn A C I I C B)))) (not (and (not (@Col Tn A B C)) (and (@CongA Tn B A I I A C) (and (@CongA Tn A B I I B C) (@CongA Tn A C I I C B))))) *)
(* Goal: or (and (not (@Col Tn A B C)) (and (@CongA Tn B A I I A C) (and (@CongA Tn A B I I B C) (@CongA Tn A C I I C B)))) (not (and (not (@Col Tn A B C)) (and (@CongA Tn B A I I A C) (and (@CongA Tn A B I I B C) (@CongA Tn A C I I C B))))) *)
(* Goal: or (and (not (@Col Tn A B C)) (and (@CongA Tn B A I I A C) (and (@CongA Tn A B I I B C) (@CongA Tn A C I I C B)))) (not (and (not (@Col Tn A B C)) (and (@CongA Tn B A I I A C) (and (@CongA Tn A B I I B C) (@CongA Tn A C I I C B))))) *)
destruct (conga_dec A C I I C B) as [HCC | HCNC].
(* Goal: and (@CongA Tn B A X X A C) (and (@CongA Tn A B X X B C) (@CongA Tn A C X X C B)) *)
left;split;auto.
(* Goal: or (and (not (@Col Tn A B C)) (and (@CongA Tn B A I I A C) (and (@CongA Tn A B I I B C) (@CongA Tn A C I I C B)))) (not (and (not (@Col Tn A B C)) (and (@CongA Tn B A I I A C) (and (@CongA Tn A B I I B C) (@CongA Tn A C I I C B))))) *)
right;intro HN.
(* Goal: False *)
destruct HN as [HNCOL1 [HCONGA [HCONGAB HCONGAC]]].
(* Goal: False *)
(* Goal: or (and (not (@Col Tn A B C)) (and (@CongA Tn B A I I A C) (and (@CongA Tn A B I I B C) (@CongA Tn A C I I C B)))) (not (and (not (@Col Tn A B C)) (and (@CongA Tn B A I I A C) (and (@CongA Tn A B I I B C) (@CongA Tn A C I I C B))))) *)
(* Goal: or (and (not (@Col Tn A B C)) (and (@CongA Tn B A I I A C) (and (@CongA Tn A B I I B C) (@CongA Tn A C I I C B)))) (not (and (not (@Col Tn A B C)) (and (@CongA Tn B A I I A C) (and (@CongA Tn A B I I B C) (@CongA Tn A C I I C B))))) *)
elim HCNC;auto.
(* Goal: or (and (not (@Col Tn A B C)) (and (@CongA Tn B A I I A C) (and (@CongA Tn A B I I B C) (@CongA Tn A C I I C B)))) (not (and (not (@Col Tn A B C)) (and (@CongA Tn B A I I A C) (and (@CongA Tn A B I I B C) (@CongA Tn A C I I C B))))) *)
right;intro HN.
(* Goal: False *)
destruct HN as [HNCOL1 [HCONGA [HCONGAB HCONGAC]]].
(* Goal: False *)
(* Goal: or (and (not (@Col Tn A B C)) (and (@CongA Tn B A I I A C) (and (@CongA Tn A B I I B C) (@CongA Tn A C I I C B)))) (not (and (not (@Col Tn A B C)) (and (@CongA Tn B A I I A C) (and (@CongA Tn A B I I B C) (@CongA Tn A C I I C B))))) *)
elim HBNC;CongA.
(* Goal: or (and (not (@Col Tn A B C)) (and (@CongA Tn B A I I A C) (and (@CongA Tn A B I I B C) (@CongA Tn A C I I C B)))) (not (and (not (@Col Tn A B C)) (and (@CongA Tn B A I I A C) (and (@CongA Tn A B I I B C) (@CongA Tn A C I I C B))))) *)
right;intro HN.
(* Goal: False *)
destruct HN as [HNCOL1 [HCONGA [HCONGAB HCONGAC]]].
(* Goal: False *)
elim HANC;auto.
Qed.

End InCenter.