Require Export GeoCoq.Tarski_dev.Ch13_1.
Require Export GeoCoq.Highschool.triangles.

Section Bisector.

Context `{TE:Tarski_euclidean}.

(** Existence of the interior bisector of an angle. *)

Lemma bisector_existence : forall A B C,  A <> B -> B <> C ->
exists E,  InAngle E A B C /\ CongA A B E E B C.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) B C)), @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@InAngle Tn E A B C) (@CongA Tn A B E E B C)) *)
intros A B C HAB HBC.
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@InAngle Tn E A B C) (@CongA Tn A B E E B C)) *)
destruct (col_dec A B C) as [HCOL | HNCOL].
(*case 1: Out B A C*)
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@InAngle Tn E A B C) (@CongA Tn A B E E B C)) *)
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@InAngle Tn E A B C) (@CongA Tn A B E E B C)) *)
destruct (out_dec B A C) as [HOUT | HNOUT].
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@InAngle Tn E A B C) (@CongA Tn A B E E B C)) *)
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@InAngle Tn E A B C) (@CongA Tn A B E E B C)) *)
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@InAngle Tn E A B C) (@CongA Tn A B E E B C)) *)
exists C.
(* Goal: and (@Bet Tn A x2 C) (or (@eq (@Tpoint Tn) x2 B) (@Out Tn B x2 I)) *)
(* Goal: @CongA Tn A B I I B C *)
split.
(* Goal: @InAngle Tn C A B C *)
(* Goal: @CongA Tn A B C C B C *)
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@InAngle Tn E A B C) (@CongA Tn A B E E B C)) *)
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@InAngle Tn E A B C) (@CongA Tn A B E E B C)) *)
apply (out_in_angle A B C C);auto.
(* Goal: @Out Tn B C A *)
(* Goal: @CongA Tn A B C C B C *)
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@InAngle Tn E A B C) (@CongA Tn A B E E B C)) *)
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@InAngle Tn E A B C) (@CongA Tn A B E E B C)) *)
apply (l6_6 B A C);auto.
(* Goal: @CongA Tn A B C C B C *)
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@InAngle Tn E A B C) (@CongA Tn A B E E B C)) *)
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@InAngle Tn E A B C) (@CongA Tn A B E E B C)) *)
apply (l11_21_b A B C C B C);auto.
(* Goal: @Out Tn B C C *)
apply (out_trivial B C);auto.
(*Case 2 Bet A B C*)
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@InAngle Tn E A B C) (@CongA Tn A B E E B C)) *)
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@InAngle Tn E A B C) (@CongA Tn A B E E B C)) *)
assert (Bet A B C) by(apply (not_out_bet A B C);auto).
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@InAngle Tn E A B C) (@CongA Tn A B E E B C)) *)
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@InAngle Tn E A B C) (@CongA Tn A B E E B C)) *)
destruct (perp_exists B A C) as [E HPerp].
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@InAngle Tn E A B C) (@CongA Tn A B E E B C)) *)
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@InAngle Tn E A B C) (@CongA Tn A B E E B C)) *)
intro HEQAC.
(* Goal: False *)
subst.
(* Goal: False *)
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@InAngle Tn E A B C) (@CongA Tn A B E E B C)) *)
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@InAngle Tn E A B C) (@CongA Tn A B E E B C)) *)
elim HAB.
(* Goal: @eq (@Tpoint Tn) C B *)
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@InAngle Tn E A B C) (@CongA Tn A B E E B C)) *)
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@InAngle Tn E A B C) (@CongA Tn A B E E B C)) *)
apply (between_identity C B); auto.
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@InAngle Tn E A B C) (@CongA Tn A B E E B C)) *)
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@InAngle Tn E A B C) (@CongA Tn A B E E B C)) *)
exists E.
(* Goal: and (@Bet Tn A x2 C) (or (@eq (@Tpoint Tn) x2 B) (@Out Tn B x2 I)) *)
(* Goal: @CongA Tn A B I I B C *)
split.
(* Goal: @InAngle Tn I A B C *)
(* Goal: @CongA Tn A B I I B C *)
unfold InAngle.
(* Goal: and (@Bet Tn A x2 C) (or (@eq (@Tpoint Tn) x2 B) (@Out Tn B x2 I)) *)
(* Goal: @CongA Tn A B I I B C *)
repeat split.
(* Goal: @Perp Tn H1 B I H1 *)
assert_diffs;auto.
(* Goal: @Perp Tn H1 B I H1 *)
assert_diffs; auto.
(* Goal: @Perp Tn H1 B I H1 *)
assert_diffs;auto.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn A X C) (or (@eq (@Tpoint Tn) X B) (@Out Tn B X E))) *)
(* Goal: @CongA Tn A B E E B C *)
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@InAngle Tn E A B C) (@CongA Tn A B E E B C)) *)
exists B.
(* Goal: @Midpoint Tn I A' C' *)
(* Goal: @Bet Tn B A C' *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn A X C) (or (@eq (@Tpoint Tn) X B) (@Out Tn B X I))) *)
(* Goal: @CongA Tn A B I I B C *)
split;auto.
(* Goal: @CongA Tn A B E E B C *)
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@InAngle Tn E A B C) (@CongA Tn A B E E B C)) *)
assert (Perp B E A B) by (apply (perp_col1 B E A C B);auto;Col).
(* Goal: @CongA Tn A B E E B C *)
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@InAngle Tn E A B C) (@CongA Tn A B E E B C)) *)
assert (Perp B E C B) by (apply (perp_col1 B E C A B);assert_diffs;auto;Perp;Col).
(* Goal: @CongA Tn A B E E B C *)
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@InAngle Tn E A B C) (@CongA Tn A B E E B C)) *)
assert (Per E B A) by (apply (perp_per_1 B E A);assert_diffs;auto;assumption).
(* Goal: @CongA Tn A B E E B C *)
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@InAngle Tn E A B C) (@CongA Tn A B E E B C)) *)
assert (Per E B C) by (apply (perp_per_2 B E C);assert_diffs;auto;Perp;Perp).
(* Goal: @CongA Tn A B E E B C *)
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@InAngle Tn E A B C) (@CongA Tn A B E E B C)) *)
assert (CongA E B A E B C) by (apply (l11_16 E B A E B C);auto;assert_diffs;auto; assert_diffs;auto).
(* Goal: @CongA Tn I B H1 I B H2 *)
(* Goal: @Out Tn B H2 C *)
(* Goal: @Out Tn B H2 C *)
CongA.
(*case 3: ~ Col A B C. *)
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@InAngle Tn E A B C) (@CongA Tn A B E E B C)) *)
destruct (segment_construction B A B C ) as [C'[ HC'1 HC'2]].
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@InAngle Tn E A B C) (@CongA Tn A B E E B C)) *)
destruct (segment_construction B C B A ) as [A' [HA'1 HA'2]].
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@InAngle Tn E A B C) (@CongA Tn A B E E B C)) *)
destruct (midpoint_existence A' C') as [I HI].
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@InAngle Tn E A B C) (@CongA Tn A B E E B C)) *)
assert (Cong B C' A' B) by (apply l2_11 with A C;Cong;Between).
(* Goal: @Coplanar Tn I B H1 H2 *)
(* Goal: @CongA Tn I B H1 I B H2 *)
(* Goal: @Out Tn B H2 C *)
(* Goal: @Out Tn B H2 C *)
assert_diffs.
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@InAngle Tn E A B C) (@CongA Tn A B E E B C)) *)
assert (CongA A' C' B C' A' B).
(* Goal: @OS Tn I B H2 C *)
(* Goal: @Out Tn B H2 C *)
 {
 apply  (isosceles_conga C' B A');auto.
(* Goal: @OS Tn I B H2 C *)
(* Goal: @Out Tn B H2 C *)
 {
(* Goal: not (@Col Tn B C I) *)
 intro.
(* Goal: False *)
 subst.
(* Goal: False *)
 treat_equalities.
(* Goal: False *)
 assert_cols.
(* Goal: False *)
 apply HNCOL.
(* Goal: @Col Tn A B C *)
  ColR. }
(* Goal: @isosceles Tn C' B A' *)
  unfold isosceles. Cong.
 }
(* Goal: @Cong Tn H1 I H2 I *)
(* Goal: @Le Tn H1 I B I *)
unfold Midpoint in *;Cong.
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@InAngle Tn E A B C) (@CongA Tn A B E E B C)) *)
destruct HI as [HBET HCONG].
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@InAngle Tn E A B C) (@CongA Tn A B E E B C)) *)
assert (HTRI : Cong I B I B /\ (I <> B -> CongA C' I B A' I B /\ CongA C' B I A' B I)).
(* Goal: @OS Tn I B H2 C *)
(* Goal: @Out Tn B H2 C *)
{ apply  (l11_49 I C' B I A' B).
(* Goal: @CongA Tn I C' B I A' B *)
(* Goal: @Cong Tn C' I A' I *)
(* Goal: @Cong Tn C' B A' B *)
 apply (out_conga A' C' B C' A' B I B I B);auto.
(* Goal: @Out Tn C' A' I *)
(* Goal: @Out Tn C' B B *)
(* Goal: @Out Tn A' C' I *)
(* Goal: @Out Tn A' B B *)
(* Goal: @Cong Tn C' I A' I *)
(* Goal: @Cong Tn C' B A' B *)
 apply (l6_6 C' I A');auto.
(* Goal: @Out Tn C' I A' *)
(* Goal: @Out Tn C' B B *)
(* Goal: @Out Tn A' C' I *)
(* Goal: @Out Tn A' B B *)
(* Goal: @Cong Tn C' I A' I *)
(* Goal: @Cong Tn C' B A' B *)
 apply (bet_out C' I A'); auto.
(* Goal: @Coplanar Tn I B H1 H2 *)
(* Goal: @CongA Tn I B H1 I B H2 *)
(* Goal: @Out Tn B H2 C *)
(* Goal: @Out Tn B H2 C *)
 assert_diffs.
(* Goal: not (@Col Tn B C I) *)
 intro.
(* Goal: False *)
 subst;treat_equalities.
(* Goal: False *)
(* Goal: @Out Tn A' B B *)
(* Goal: @Cong Tn C' I A' I *)
(* Goal: @Cong Tn C' B A' B *)
 elim H6; auto.
(* Goal: @Perp Tn H1 B I H1 *)
 assert_diffs;auto.
(* Goal: @Bet Tn B A C' *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn A X C) (or (@eq (@Tpoint Tn) X B) (@Out Tn B X I))) *)
(* Goal: @CongA Tn A B I I B C *)
 Between.
(* Goal: @Out Tn C' B B *)
(* Goal: @Out Tn A' C' I *)
(* Goal: @Out Tn A' B B *)
(* Goal: @Cong Tn C' I A' I *)
(* Goal: @Cong Tn C' B A' B *)
 apply (out_trivial C' B);auto.
(* Goal: @Out Tn A' C' I *)
(* Goal: @Out Tn A' B B *)
(* Goal: @Cong Tn C' I A' I *)
(* Goal: @Cong Tn C' B A' B *)
 apply (l6_6 A' I C');auto.
(* Goal: @Out Tn A' I C' *)
(* Goal: @Out Tn A' B B *)
(* Goal: @Cong Tn C' I A' I *)
(* Goal: @Cong Tn C' B A' B *)
 apply (bet_out A' I C'); auto.
(* Goal: @Coplanar Tn I B H1 H2 *)
(* Goal: @CongA Tn I B H1 I B H2 *)
(* Goal: @Out Tn B H2 C *)
(* Goal: @Out Tn B H2 C *)
 assert_diffs.
(* Goal: False *)
 intro; subst;treat_equalities.
(* Goal: False *)
(* Goal: @Out Tn A' B B *)
(* Goal: @Cong Tn C' I A' I *)
(* Goal: @Cong Tn C' B A' B *)
 elim H6; auto.
(* Goal: @Perp Tn H1 B I H1 *)
 assert_diffs;auto.
(* Goal: @Out Tn A' B B *)
(* Goal: @Cong Tn C' I A' I *)
(* Goal: @Cong Tn C' B A' B *)
 apply (out_trivial A' B); auto.
(* Goal: @Cong Tn H1 I H2 I *)
(* Goal: @Le Tn H1 I B I *)
 Cong.
(* Goal: @Cong Tn H1 I H2 I *)
(* Goal: @Le Tn H1 I B I *)
 Cong. 
}
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@InAngle Tn E A B C) (@CongA Tn A B E E B C)) *)
exists I.
(* Goal: and (@InAngle Tn I A B C) (@CongA Tn A B I I B C) *)
destruct HTRI as [HCONGIB HIBO].
(* Goal: and (@InAngle Tn I A B C) (@CongA Tn A B I I B C) *)
assert (I <> B) by (intro;elim HNCOL;ColR).
(* Goal: and (@InAngle Tn I A B C) (@CongA Tn A B I I B C) *)
assert (CongA A B I I B C).
(* Goal: @OS Tn I B H2 C *)
(* Goal: @Out Tn B H2 C *)
{ apply (out_conga C' B I I B A' A I I C).
(* Goal: @CongA Tn C' B I I B A' *)
(* Goal: @Out Tn B C' A *)
(* Goal: @Out Tn B I I *)
(* Goal: @Out Tn B I I *)
(* Goal: @Out Tn B A' C *)
  apply (conga_right_comm C' B I A' B I).
(* Goal: @CongA Tn C' B I A' B I *)
(* Goal: @Out Tn B C' A *)
(* Goal: @Out Tn B I I *)
(* Goal: @Out Tn B I I *)
(* Goal: @Out Tn B A' C *)
  apply HIBO;auto.
(* Goal: @Out Tn B C' A *)
(* Goal: @Out Tn B I I *)
(* Goal: @Out Tn B I I *)
(* Goal: @Out Tn B A' C *)
  apply (l6_6 B A C').
(* Goal: @Out Tn B A C' *)
(* Goal: @Out Tn B I I *)
(* Goal: @Out Tn B I I *)
(* Goal: @Out Tn B A' C *)
  apply (bet_out B A C').
(* Goal: not (@eq (@Tpoint Tn) C B) *)
(* Goal: @Bet Tn B C A' *)
  intuition.
(* Goal: @CongA Tn A B I I B C *)
  assumption.
(* Goal: @Out Tn B I I *)
(* Goal: @Out Tn B C C *)
  apply (out_trivial B I);auto.
(* Goal: @Out Tn B I I *)
(* Goal: @Out Tn B C C *)
  apply (out_trivial B I);auto.
(* Goal: @Out Tn B A' C *)
  apply (l6_6 B C A').
(* Goal: @Out Tn B C A' *)
  apply (bet_out B C A').
(* Goal: not (@eq (@Tpoint Tn) C B) *)
(* Goal: @Bet Tn B C A' *)
  intuition.
(* Goal: @CongA Tn A B I I B C *)
  assumption.
}
(* Goal: and (@Bet Tn A x2 C) (or (@eq (@Tpoint Tn) x2 B) (@Out Tn B x2 I)) *)
(* Goal: @CongA Tn A B I I B C *)
split.
(* Goal: @InAngle Tn I A B C *)
(* Goal: @CongA Tn A B I I B C *)
unfold InAngle.
(* Goal: and (@Bet Tn A x2 C) (or (@eq (@Tpoint Tn) x2 B) (@Out Tn B x2 I)) *)
(* Goal: @CongA Tn A B I I B C *)
repeat split.
(* Goal: @Perp Tn H1 B I H1 *)
assert_diffs;auto.
(* Goal: @Perp Tn H1 B I H1 *)
assert_diffs;auto.
(* Goal: @CongA Tn A B I I B C *)
assumption.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn A X C) (or (@eq (@Tpoint Tn) X B) (@Out Tn B X I))) *)
(* Goal: @CongA Tn A B I I B C *)
destruct (inner_pasch A' B C' I A) as [x1 HIN1].
(* Goal: @Bet Tn A' I C' *)
(* Goal: @Bet Tn B A C' *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn A X C) (or (@eq (@Tpoint Tn) X B) (@Out Tn B X I))) *)
(* Goal: @CongA Tn A B I I B C *)
apply (midpoint_bet A' I C');auto.
(* Goal: @Midpoint Tn I A' C' *)
(* Goal: @Bet Tn B A C' *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn A X C) (or (@eq (@Tpoint Tn) X B) (@Out Tn B X I))) *)
(* Goal: @CongA Tn A B I I B C *)
split;auto.
(* Goal: @Bet Tn B A C' *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn A X C) (or (@eq (@Tpoint Tn) X B) (@Out Tn B X I))) *)
(* Goal: @CongA Tn A B I I B C *)
Between.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn A X C) (or (@eq (@Tpoint Tn) X B) (@Out Tn B X I))) *)
(* Goal: @CongA Tn A B I I B C *)
destruct HIN1 as [HIN11 HIN12].
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn A X C) (or (@eq (@Tpoint Tn) X B) (@Out Tn B X I))) *)
(* Goal: @CongA Tn A B I I B C *)
destruct (inner_pasch A B A' x1 C) as [x2 HIN2];auto.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn A X C) (or (@eq (@Tpoint Tn) X B) (@Out Tn B X I))) *)
(* Goal: @CongA Tn A B I I B C *)
exists x2.
(* Goal: and (@Bet Tn A x2 C) (or (@eq (@Tpoint Tn) x2 B) (@Out Tn B x2 I)) *)
(* Goal: @CongA Tn A B I I B C *)
destruct HIN2 as [HIN21 HIN22].
(* Goal: and (@Bet Tn A x2 C) (or (@eq (@Tpoint Tn) x2 B) (@Out Tn B x2 I)) *)
(* Goal: @CongA Tn A B I I B C *)
split.
(* Goal: @Bet Tn A x2 C *)
(* Goal: or (@eq (@Tpoint Tn) x2 B) (@Out Tn B x2 I) *)
(* Goal: @CongA Tn A B I I B C *)
apply (Bet_cases A x2 C).
(* Goal: or (@Bet Tn A x2 C) (@Bet Tn C x2 A) *)
(* Goal: or (@eq (@Tpoint Tn) x2 B) (@Out Tn B x2 I) *)
(* Goal: @CongA Tn A B I I B C *)
right;auto.
(* Goal: or (@eq (@Tpoint Tn) x2 B) (@Out Tn B x2 I) *)
(* Goal: @CongA Tn A B I I B C *)
right.
(* Goal: @Out Tn B x2 I *)
(* Goal: @CongA Tn A B I I B C *)
apply (bet_out B x2 I).
(* Goal: not (@Col Tn B C I) *)
intro.
(* Goal: @Col Tn A B C *)
elim HNCOL;ColR.
(* Goal: @Bet Tn B x2 I *)
(* Goal: @CongA Tn A B I I B C *)
bet.
(* Goal: @CongA Tn A B I I B C *)
assumption.
Qed.

Lemma not_col_bfoot_not_equality : forall A B C I H1 H2, ~ Col A B C -> Coplanar A B C I ->
Col A B H1 -> Col B C H2 -> CongA A B I I B C->
Perp A B I H1 -> Perp B C I H2 -> H1 <> B /\ H2 <> B.
Proof.
intros A B C I H1 H2 HNCOL HCOP HCOL1 HCOL2 HCONGA HORTHA HORTHC.
(* Goal: and (@Bet Tn A x2 C) (or (@eq (@Tpoint Tn) x2 B) (@Out Tn B x2 I)) *)
(* Goal: @CongA Tn A B I I B C *)
split.
(* Goal: not (@Col Tn B C I) *)
intro.
(* Goal: False *)
subst.
assert (Per A B I) by (apply (perp_per_1 B A I);auto;assert_diffs;auto;Perp).
assert (Col A C B).
(* Goal: @OS Tn I B H2 C *)
(* Goal: @Out Tn B H2 C *)
{  apply cop_per2__col with I;Cop.
(* Goal: @Perp Tn H1 B I H1 *)
  assert_diffs;auto.
  apply (l8_2 I B C);auto.
  apply (l11_17 A B I I B C);auto. }
elim HNCOL;Col.
(* Goal: False *)
intro;subst.
assert (Per C B I) by (apply (perp_per_1 B C I);auto;assert_diffs;auto).
assert (Per I B C) by (apply (l8_2 C B I);auto).
assert (Col A C B).
(* Goal: @OS Tn I B H2 C *)
(* Goal: @Out Tn B H2 C *)
{ apply cop_per2__col with I;Cop.
(* Goal: @Perp Tn H1 B I H1 *)
  assert_diffs; auto.
 apply (l11_17 I B C A B I);auto.
(* Goal: @CongA Tn I B H1 I B H2 *)
(* Goal: @Out Tn B H2 C *)
(* Goal: @Out Tn B H2 C *)
 CongA. }
elim HNCOL; Col.
Qed.

Lemma bisector_foot_out_out : forall A B C I H1 H2, ~ Col A B C ->
Coplanar A B C I -> Col A B H1 -> Col B C H2-> CongA A B I I B C->
Perp A B I H1 -> Perp B C I H2 -> (Out B H1 A -> Out B H2 C).
Proof.
(* Goal: forall (A B C I H1 H2 : @Tpoint Tn) (_ : not (@Col Tn A B C)) (_ : @Coplanar Tn A B C I) (_ : @Col Tn A B H1) (_ : @Col Tn B C H2) (_ : @CongA Tn A B I I B C) (_ : @Perp Tn A B I H1) (_ : @Perp Tn B C I H2) (_ : @Out Tn B H1 A), @Out Tn B H2 C *)
intros A B C I H1 H2 HNCOL HCOP HCOL1 HCOL2 HCONGA HORTHA HORTHC HOUT1.
(* Goal: @Out Tn B H2 C *)
destruct (not_col_bfoot_not_equality A B C I H1 H2) as [HNEQH1 HNEQH2];auto.
(* Goal: @Out Tn B H2 C *)
assert (Acute H1 B I). 
(* Goal: @OS Tn I B H2 C *)
(* Goal: @Out Tn B H2 C *)
{ apply (perp_out_acute H1 B I H1);auto. 
(* Goal: @Out Tn B H1 H1 *)
(* Goal: @Perp Tn H1 B I H1 *)
  apply (out_trivial B H1);auto.
(* Goal: @Perp Tn H1 B I H1 *)
  apply (perp_col2 A B H1 B I H1);auto.
  Col. }
(* Goal: @Out Tn B H2 C *)
assert (CongA H1 B I I B C).
(* Goal: @OS Tn I B H2 C *)
(* Goal: @Out Tn B H2 C *)
{ apply (out_conga A B I I B C H1 I I C);auto.
(* Goal: @Out Tn B A H1 *)
(* Goal: @Out Tn B I I *)
(* Goal: @Out Tn B I I *)
(* Goal: @Out Tn B C C *)
  apply (l6_6 B H1 A);auto.
(* Goal: @Out Tn B I I *)
(* Goal: @Out Tn B C C *)
  apply (out_trivial B I);auto.
(* Goal: @Perp Tn H1 B I H1 *)
  assert_diffs;auto.
(* Goal: @Out Tn B I I *)
(* Goal: @Out Tn B C C *)
  apply (out_trivial B I);auto.
(* Goal: @Perp Tn H1 B I H1 *)
  assert_diffs;auto.
(* Goal: @Out Tn B C C *)
  apply (out_trivial B C);auto.
(* Goal: @Perp Tn H1 B I H1 *)
  assert_diffs;auto. }
(* Goal: @Out Tn B H2 C *)
assert (Acute I B C) by (apply (acute_conga__acute H1 B I I B C);auto).
(* Goal: @Out Tn B H2 C *)
apply (acute_col_perp__out I B C H2);auto.
Qed.

Lemma not_col_efoot_not_equality : forall A B C I H1 H2, ~ Col A B C -> Coplanar A B C I ->
Col A B H1 -> Col B C H2-> Cong I H1 I H2->
Perp A B I H1 -> Perp B C I H2 -> H1 <> B /\ H2 <> B.
Proof.
intros A B C I H1 H2 HNCOL HCOP HCOLH1 HCOLH2 HCONG HPERH1 HPERH2.
assert (H1 <> B).
(* Goal: not (@Col Tn B C I) *)
intro.
(* Goal: False *)
subst.
assert (H2 <> B).
(* Goal: @OS Tn I B H2 C *)
(* Goal: @Out Tn B H2 C *)
{  intro.
(* Goal: False *)
  subst.
  assert (Col B A C).
   apply (cop_perp2__col B A C I B);auto.
(* Goal: @Coplanar Tn A B C I *)
(* Goal: @Out Tn B H2 C *)
  Cop.
(* Goal: @Perp Tn H1 B I H1 *)
  Perp.
  elim HNCOL.
(* Goal: @Col Tn B H2 C *)
(* Goal: @OS Tn B I H2 C *)
  Col.
}
assert (Perp B H2 I H2).
  apply (perp_col B C I H2 H2);auto.
assert (Per B H2 I).
(* Goal: @OS Tn I B H2 C *)
(* Goal: @Out Tn B H2 C *)
{  apply (perp_per_1 H2 B I);auto.
(* Goal: @Perp Tn H1 B I H1 *)
   Perp.
}
assert (Per H2 B I).
(* Goal: @OS Tn I B H2 C *)
(* Goal: @Out Tn B H2 C *)
{
  apply (l11_17 B H2 I H2 B I);auto.
  apply (isosceles_conga H2 I B);auto.
(* Goal: @Perp Tn H1 B I H1 *)
  assert_diffs;auto.
(* Goal: @Cong Tn H1 I H2 I *)
(* Goal: @Le Tn H1 I B I *)
  unfold isosceles;Cong.
}
assert (H2 = B).
(* Goal: @OS Tn I B H2 C *)
(* Goal: @Out Tn B H2 C *)
{
  apply (l8_7 I H2 B);auto.
  apply (l8_2 B H2 I);auto.
  apply (l8_2 H2 B I);auto.
}
contradiction.
(* Goal: @Midpoint Tn I A' C' *)
(* Goal: @Bet Tn B A C' *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn A X C) (or (@eq (@Tpoint Tn) X B) (@Out Tn B X I))) *)
(* Goal: @CongA Tn A B I I B C *)
split;auto.
(* Goal: not (@Col Tn B C I) *)
intro.
(* Goal: False *)
subst.
(* Goal: @Perp Tn H1 B I H1 *)
assert (Perp B H1 I H1) by (apply (perp_col B A I H1 H1);auto;Perp;Col).
assert (Per B H1 I) by (apply (perp_per_1 H1 B I);auto;Perp).
assert (Per H1 B I).
(* Goal: @OS Tn I B H2 C *)
(* Goal: @Out Tn B H2 C *)
{
  apply (l11_17 B H1 I H1 B I);auto.
  apply (isosceles_conga H1 I B);auto.
(* Goal: @Perp Tn H1 B I H1 *)
  assert_diffs;auto.
(* Goal: @Cong Tn H1 I H2 I *)
(* Goal: @Le Tn H1 I B I *)
  unfold isosceles;Cong.
}
assert (H1 = B).
(* Goal: @OS Tn I B H2 C *)
(* Goal: @Out Tn B H2 C *)
{
  apply (l8_7 I H1 B);auto.
  apply (l8_2 B H1 I);auto.
  apply (l8_2 H1 B I);auto.
}
contradiction.
Qed.

End Bisector.


Ltac col_with_conga := 
match goal with
   | H: (CongA ?A ?B ?I ?I ?B ?C) |- Col ?A ?B ?C => 
      assert (Col A B I) by (assert_diffs;ColR); assert (HH : Col I B C) by (apply (col_conga_col A B I I B C);assumption);
      assert_diffs;ColR
   | H :(CongA ?A ?B ?I ?C ?B ?I) |- Col ?A ?B ?C => 
      assert (CongA A B I I B C) by (apply (conga_right_comm A B I C B I);assumption); col_with_conga
   | H :(CongA ?I ?B ?A ?I ?B ?C) |- Col ?A ?B ?C => 
      assert (CongA A B I I B C) by (apply (conga_left_comm I B A I B C);assumption); col_with_conga
   | H :(CongA ?I ?B ?A ?C ?B ?I) |- Col ?A ?B ?C => 
      assert (CongA A B I C B I) by (apply (conga_left_comm I B A C B I);assumption); col_with_conga
   | H :(CongA ?I ?B ?C ?A ?B ?I) |- Col ?A ?B ?C =>
      assert (CongA A B I I B C) by (apply (conga_sym I B C A B I);assumption); col_with_conga
   | H :(CongA ?C ?B ?I ?A ?B ?I) |- Col ?A ?B ?C =>
      assert (CongA A B I C B I) by (apply (conga_sym C B I A B I);assumption); col_with_conga
   | H :(CongA ?I ?B ?C ?I ?B ?A) |- Col ?A ?B ?C =>
      assert (CongA I B A I B C) by (apply (conga_sym I B C I B A);assumption); col_with_conga
   | H: (CongA ?C ?B ?I ?I ?B ?A) |- Col ?A ?B ?C =>
      assert (CongA I B A C B I) by (apply (conga_sym C B I I B A);assumption); col_with_conga
   | H: (CongA ?A ?B ?I ?I ?B ?C) |- Col ?C ?B ?A => 
      apply (col_permutation_3 A B C);auto;col_with_conga
   | H :(CongA ?A ?B ?I ?C ?B ?I) |- Col ?C ?B ?A => 
      apply (col_permutation_3 A B C);auto;col_with_conga
   | H :(CongA ?I ?B ?A ?I ?B ?C) |- Col ?C ?B ?A => 
      apply (col_permutation_3 A B C);auto;col_with_conga
   | H :(CongA ?I ?B ?A ?C ?B ?I) |- Col ?C ?B ?A => 
      apply (col_permutation_3 A B C);auto;col_with_conga
   | H :(CongA ?I ?B ?C ?A ?B ?I) |- Col ?C ?B ?A =>
      apply (col_permutation_3 A B C);auto;col_with_conga
   | H :(CongA ?C ?B ?I ?A ?B ?I) |- Col ?C ?B ?A =>
      apply (col_permutation_3 A B C);auto;col_with_conga
   | H :(CongA ?I ?B ?C ?I ?B ?A) |- Col ?C ?B ?A =>
      apply (col_permutation_3 A B C);auto;col_with_conga
   | H: (CongA ?C ?B ?I ?I ?B ?A) |- Col ?C ?B ?A =>
      apply (col_permutation_3 A B C);auto;col_with_conga
end.

Section Bisector_2.

Context `{TE:Tarski_euclidean}.

Lemma equality_foot_out_out : forall A B C I H1 H2, 
 ~ Col A B C -> InAngle I A B C ->
 Col A B H1 -> Col B C H2-> Cong I H1 I H2->
 Perp A B I H1 -> Perp B C I H2 -> 
 (Out B H1 A -> Out B H2 C).
Proof.
(* Goal: forall (A B C I H1 H2 : @Tpoint Tn) (_ : not (@Col Tn A B C)) (_ : @InAngle Tn I A B C) (_ : @Col Tn A B H1) (_ : @Col Tn B C H2) (_ : @Cong Tn I H1 I H2) (_ : @Perp Tn A B I H1) (_ : @Perp Tn B C I H2) (_ : @Out Tn B H1 A), @Out Tn B H2 C *)
intros A B C I H1 H2 HNCOL HINANGLE HCOLH1 HCOLH2 HCONG HPERH1 HPERH2 HOUTH1.
(* Goal: @Out Tn B H2 C *)
destruct (not_col_efoot_not_equality A B C I H1 H2) as [HNEQH1 HNEQH2];auto.
(* Goal: @Coplanar Tn A B C I *)
(* Goal: @Out Tn B H2 C *)
 Cop.
(* Goal: @Out Tn B H2 C *)
assert(HMY : Cong H1 B H2 B /\ CongA H1 B I H2 B I /\ CongA H1 I B H2 I B).
(* Goal: @OS Tn I B H2 C *)
(* Goal: @Out Tn B H2 C *)
{  apply (l11_52 B H1 I B H2 I).
(* Goal: @CongA Tn B H1 I B H2 I *)
(* Goal: @Cong Tn B I B I *)
(* Goal: @Cong Tn H1 I H2 I *)
(* Goal: @Le Tn H1 I B I *)
   apply (l11_16 B H1 I B H2 I).
(* Goal: @Per Tn B H1 I *)
   apply (perp_per_1 H1 B I).
(* Goal: @Perp Tn H1 B I H1 *)
   assert_diffs;auto.
(* Goal: @Perp Tn H1 B I H1 *)
   assert (Perp B H1 I H1) by (apply (perp_col B A I H1 H1);auto;Perp;Col).
(* Goal: @Perp Tn H1 B I H1 *)
   Perp.
(* Goal: @Perp Tn H1 B I H1 *)
   assert_diffs;auto.
(* Goal: @Perp Tn H1 B I H1 *)
   assert_diffs;auto.
(* Goal: @Per Tn B H2 I *)
(* Goal: not (@eq (@Tpoint Tn) B H2) *)
(* Goal: not (@eq (@Tpoint Tn) I H2) *)
(* Goal: @Cong Tn B I B I *)
(* Goal: @Cong Tn H1 I H2 I *)
(* Goal: @Le Tn H1 I B I *)
   apply (perp_per_1 H2 B I).
(* Goal: @Perp Tn H1 B I H1 *)
   assert_diffs;auto.
(* Goal: @Perp Tn H2 B I H2 *)
(* Goal: not (@eq (@Tpoint Tn) B H2) *)
(* Goal: not (@eq (@Tpoint Tn) I H2) *)
(* Goal: @Cong Tn B I B I *)
(* Goal: @Cong Tn H1 I H2 I *)
(* Goal: @Le Tn H1 I B I *)
   assert (Perp B H2 I H2) by (apply (perp_col B C I H2 H2);auto;Perp;Col).
(* Goal: @Perp Tn H1 B I H1 *)
   Perp.
(* Goal: @Perp Tn H1 B I H1 *)
   assert_diffs;auto.
(* Goal: @Perp Tn H1 B I H1 *)
   assert_diffs;auto.
(* Goal: @Cong Tn H1 I H2 I *)
(* Goal: @Le Tn H1 I B I *)
   Cong.
(* Goal: @Cong Tn H1 I H2 I *)
(* Goal: @Le Tn H1 I B I *)
   Cong.
(* Goal: @Coplanar Tn I B H1 H2 *)
(* Goal: @CongA Tn I B H1 I B H2 *)
(* Goal: @Out Tn B H2 C *)
(* Goal: @Out Tn B H2 C *)
   assert_diffs.
(* Goal: @Le Tn H1 I B I *)
   apply (l11_46 B H1 I); auto.
(* Goal: or (@Per Tn B H1 I) (@Obtuse Tn B H1 I) *)
   left.
(* Goal: @Per Tn B H1 I *)
   apply (perp_per_1 H1 B I).
(* Goal: @Perp Tn H1 B I H1 *)
   assert_diffs;auto.
(* Goal: @Perp Tn H1 B I H1 *)
   assert (Perp B H1 I H1) by (apply (perp_col B A I H1 H1);auto;Perp;Col).
   Perp.  }
(* Goal: @Out Tn B H2 C *)
destruct HMY as [HSH1BH2B [HAH1BI HAH1IB]].
(* Goal: @Out Tn B H2 C *)
assert (TS I B A C).
(* Goal: @OS Tn I B H2 C *)
(* Goal: @Out Tn B H2 C *)
{  apply (in_angle_two_sides A B C I);auto.
(* Goal: not (@Col Tn B C I) *)
   intro.
(* Goal: False *)
(* Goal: not (@Col Tn B C I) *)
   assert (Col H1 B H2) by (col_with_conga).
(* Goal: @Col Tn A B C *)
   elim HNCOL; ColR.
(* Goal: not (@Col Tn B C I) *)
   intro.
(* Goal: False *)
   assert (Col H2 B H1) by (col_with_conga).
(* Goal: @Col Tn A B C *)
   elim HNCOL;ColR. }
(* Goal: @Out Tn B H2 C *)
destruct (conga_cop__or_out_ts I B H1 H2) as [HOUTH1H2 | HTSH1H2].
(* Goal: @Coplanar Tn I B H1 H2 *)
(* Goal: @CongA Tn I B H1 I B H2 *)
(* Goal: @Out Tn B H2 C *)
(* Goal: @Out Tn B H2 C *)
assert_diffs.
(* Goal: @Col Tn B H2 C *)
(* Goal: @OS Tn B I H2 C *)
apply coplanar_perm_2, col_cop__cop with C; Col.
(* Goal: @Coplanar Tn A B C I *)
(* Goal: @Out Tn B H2 C *)
apply coplanar_perm_5, col_cop__cop with A; Col; Cop.
(* Goal: @CongA Tn I B H1 I B H2 *)
(* Goal: @Out Tn B H2 C *)
(* Goal: @Out Tn B H2 C *)
CongA.
(* Goal: @Col Tn A B C *)
elim HNCOL;ColR.
(* Goal: @Out Tn B H2 C *)
assert (TS I B A H2) by (apply (l9_5 I B H1 H2 B A);auto;Col).
(* Goal: @Out Tn B H2 C *)
assert (OS I B H2 C).
(* Goal: @OS Tn I B H2 C *)
(* Goal: @Out Tn B H2 C *)
{ apply (l9_8_1 I B H2 C A);auto.
(* Goal: @TS Tn I B H2 A *)
(* Goal: @TS Tn I B C A *)
 apply (l9_2 I B A H2);auto.
 apply (l9_2 I B A C);auto. }
(* Goal: @Out Tn B H2 C *)
apply (col_one_side_out B I H2 C);auto.
(* Goal: @Col Tn B H2 C *)
(* Goal: @OS Tn B I H2 C *)
Col.
(* Goal: @OS Tn B I H2 C *)
apply (invert_one_side I B H2 C);auto.
Qed.

(** The points on the bisector of an angle are at equal distances of the two sides. *)

Lemma bisector_perp_equality : forall A B C I H1 H2, Coplanar A B C I ->
 Col B H1 A -> Col B H2 C ->
 Perp A B I H1 -> Perp B C I H2 ->
 CongA A B I I B C ->  Cong I H1 I H2.
Proof.
intros A B C I H1 H2 HCOP HCABH HCCBH HPH1 HPH2 HCONGA.
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@InAngle Tn E A B C) (@CongA Tn A B E E B C)) *)
destruct (col_dec A B C) as [HCOL | HNCOL].
assert (Perp A B I H2) by(apply (perp_col2 B C A B I H2);auto;assert_diffs;auto;Col;Col).
assert (H1 = H2).
(* Goal: @OS Tn I B H2 C *)
(* Goal: @Out Tn B H2 C *)
{ apply (l8_14_2_1b H1 A B I H1 H2);auto.
 apply (l8_14_2_1b_bis A B I H1 H1);auto.
(* Goal: @Col Tn B H2 C *)
(* Goal: @OS Tn B I H2 C *)
 Col.
(* Goal: @Col Tn B H2 C *)
(* Goal: @OS Tn B I H2 C *)
 Col.
(* Goal: @Col Tn A B C *)
 assert_diffs; ColR.
 assert (Perp I H1 A B) by (Perp).
 assert (Perp I H2 A B) by (Perp).
 assert (Col I H1 H2) by (apply (cop_perp2__col I H1 H2 A B); Cop).
 Col. }
(* Goal: @Cong Tn H1 I H2 I *)
(* Goal: @Le Tn H1 I B I *)
subst;Cong.
(*for Col A B C End*)
(* Goal: @Out Tn B H2 C *)
destruct (not_col_bfoot_not_equality A B C I H1 H2) as [HNEQH1 HNEQH2];auto.
(* Goal: @Col Tn B H2 C *)
(* Goal: @OS Tn B I H2 C *)
 Col.
(* Goal: @Col Tn B H2 C *)
(* Goal: @OS Tn B I H2 C *)
 Col.
destruct (out_dec B H1 A) as [HOUT | HNOUT].
assert (Out B H2 C) by (apply (bisector_foot_out_out A B C I H1 H2);auto;Col;Col).
apply (l11_50_2 I B H1 I B H2).
(* Goal: @OS Tn I B H2 C *)
(* Goal: @Out Tn B H2 C *)
{ intro.
  elim HNCOL.
  col_with_conga. }
(* Goal: @OS Tn I B H2 C *)
(* Goal: @Out Tn B H2 C *)
{ apply (l11_16 B H1 I B H2 I);auto.
  apply (perp_per_1 H1 B I);auto.
(* Goal: @Perp Tn H1 B I H1 *)
  apply (perp_col2 A B H1 B I H1);auto.
(* Goal: @Col Tn B H2 C *)
(* Goal: @OS Tn B I H2 C *)
  Col.
(* Goal: @Col Tn B H2 C *)
(* Goal: @OS Tn B I H2 C *)
  Col.
(* Goal: @Perp Tn H1 B I H1 *)
  assert_diffs;auto.
  assert (Perp B H2 I H2) by (apply (perp_col B C I H2 H2);auto;Col).
  assert (Perp H2 B I H2) by (Perp).
  apply (perp_per_1 H2 B I);auto.
(* Goal: @Perp Tn H1 B I H1 *)
  assert_diffs;auto. }
assert (CongA H1 B I I B H2).
(* Goal: @OS Tn I B H2 C *)
(* Goal: @Out Tn B H2 C *)
{ apply (out_conga A B I I B C H1 I I H2);auto.
(* Goal: @Out Tn B A H1 *)
(* Goal: @Out Tn B I I *)
(* Goal: @Out Tn B I I *)
(* Goal: @Out Tn B C C *)
  apply (l6_6 B H1 A);auto.
(* Goal: @Out Tn B I I *)
(* Goal: @Out Tn B C C *)
  apply (out_trivial B I);auto.
(* Goal: @Perp Tn H1 B I H1 *)
  assert_diffs;auto.
(* Goal: @Out Tn B I I *)
(* Goal: @Out Tn B C C *)
  apply (out_trivial B I);auto.
(* Goal: @Perp Tn H1 B I H1 *)
  assert_diffs;auto.
  apply (l6_6 B H2 C);auto.
}
(* Goal: @CongA Tn I B H1 I B H2 *)
(* Goal: @Out Tn B H2 C *)
(* Goal: @Out Tn B H2 C *)
CongA.
(* Goal: @Cong Tn H1 I H2 I *)
(* Goal: @Le Tn H1 I B I *)
Cong.

destruct (symmetric_point_construction A B) as [A' HCONHA'].
destruct (symmetric_point_construction C B) as [C' HCONHC'].
assert (Bet A B A') by (apply (midpoint_bet A B A');auto).
assert (Bet C B C') by (apply (midpoint_bet C B C');auto).
assert (Out B H1 A').
(* Goal: @OS Tn I B H2 C *)
(* Goal: @Out Tn B H2 C *)
{
  assert (Bet A B H1).
   apply (not_out_bet A B H1);auto.
(* Goal: @Col Tn B H2 C *)
(* Goal: @OS Tn B I H2 C *)
   Col.
(* Goal: not (@Col Tn B C I) *)
  intro.
  elim HNOUT.
  apply (l6_6 B A H1);auto.
  apply (l6_3_2 H1 A' B);auto.
(* Goal: and (@Bet Tn A x2 C) (or (@eq (@Tpoint Tn) x2 B) (@Out Tn B x2 I)) *)
(* Goal: @CongA Tn A B I I B C *)
  repeat split.
(* Goal: @Perp Tn H1 B I H1 *)
  assert_diffs;auto.
(* Goal: @Perp Tn H1 B I H1 *)
  assert_diffs;auto.
  exists A.
(* Goal: and (@Bet Tn A x2 C) (or (@eq (@Tpoint Tn) x2 B) (@Out Tn B x2 I)) *)
(* Goal: @CongA Tn A B I I B C *)
  repeat split.
(* Goal: @Perp Tn H1 B I H1 *)
  assert_diffs;auto.
(* Goal: @Bet Tn B A C' *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn A X C) (or (@eq (@Tpoint Tn) X B) (@Out Tn B X I))) *)
(* Goal: @CongA Tn A B I I B C *)
  Between.
  Between. }
assert (Out B H2 C').
(* Goal: @OS Tn I B H2 C *)
(* Goal: @Out Tn B H2 C *)
{
  apply (bisector_foot_out_out A' B C' I H1 H2);auto.
(* Goal: not (@Col Tn B C I) *)
  intro.
  elim HNCOL.
(* Goal: @Perp Tn H1 B I H1 *)
  assert_diffs;auto.
(* Goal: @Col Tn A B C *)
  ColR.
(* Goal: @Coplanar Tn I B H1 H2 *)
(* Goal: @CongA Tn I B H1 I B H2 *)
(* Goal: @Out Tn B H2 C *)
(* Goal: @Out Tn B H2 C *)
  assert_diffs.
(* Goal: @Col Tn B H2 C *)
(* Goal: @OS Tn B I H2 C *)
  apply coplanar_perm_3, col_cop__cop with C; Col.
(* Goal: @Coplanar Tn A B C I *)
(* Goal: @Out Tn B H2 C *)
  apply coplanar_perm_19, col_cop__cop with A; Col; Cop.
(* Goal: @Col Tn B H2 C *)
(* Goal: @OS Tn B I H2 C *)
  Col.
(* Goal: @Perp Tn H1 B I H1 *)
  assert_diffs;auto.
(* Goal: @Col Tn A B C *)
  ColR.
  apply (conga_right_comm A' B I C' B I);auto.
  apply (l11_13 A B I C B I A' C');auto.
(* Goal: @CongA Tn I B H1 I B H2 *)
(* Goal: @Out Tn B H2 C *)
(* Goal: @Out Tn B H2 C *)
  CongA.
(* Goal: @Perp Tn H1 B I H1 *)
  assert_diffs;auto.
(* Goal: @Perp Tn H1 B I H1 *)
  assert_diffs;auto.
  apply (perp_col2 A B A' B I H1);auto.
(* Goal: @Perp Tn H1 B I H1 *)
  assert_diffs;auto.
(* Goal: @Col Tn B H2 C *)
(* Goal: @OS Tn B I H2 C *)
  Col.
(* Goal: @Col Tn B H2 C *)
(* Goal: @OS Tn B I H2 C *)
  Col.
  apply (perp_col2 B C B C' I H2);auto.
(* Goal: @Perp Tn H1 B I H1 *)
  assert_diffs;auto.
(* Goal: @Col Tn B H2 C *)
(* Goal: @OS Tn B I H2 C *)
  Col.
  Col. }
apply (l11_50_2 I B H1 I B H2).
(* Goal: @OS Tn I B H2 C *)
(* Goal: @Out Tn B H2 C *)
{ intro;elim HNCOL.
  col_with_conga. }
assert (Per B H1 I).
(* Goal: @OS Tn I B H2 C *)
(* Goal: @Out Tn B H2 C *)
{  apply (perp_per_1 H1 B I);auto.
(* Goal: @Perp Tn H1 B I H1 *)
   apply (perp_col2 A B H1 B I H1);auto.
(* Goal: @Col Tn B H2 C *)
(* Goal: @OS Tn B I H2 C *)
   Col.
   Col. }
assert (Per B H2 I) by (apply (perp_per_1 H2 B I);auto;
    assert (Perp B H2 I H2) by (apply (perp_col B C I H2 H2);auto;Col);Perp).
apply (l11_16 B H1 I B H2 I);auto.
(* Goal: @Perp Tn H1 B I H1 *)
 assert_diffs;auto.
(* Goal: @Perp Tn H1 B I H1 *)
 assert_diffs;auto.
assert (CongA H1 B I I B H2).
(* Goal: @OS Tn I B H2 C *)
(* Goal: @Out Tn B H2 C *)
{ apply (out_conga A' B I I B C' H1 I I H2);auto.
  assert (CongA A' B I C' B I) by (apply (l11_13 A B I C B I A' C');auto;
          CongA;assert_diffs;auto; assert_diffs;auto).
(* Goal: @CongA Tn I B H1 I B H2 *)
(* Goal: @Out Tn B H2 C *)
(* Goal: @Out Tn B H2 C *)
  CongA.
  apply (l6_6 B H1 A');auto.
(* Goal: @Out Tn B I I *)
(* Goal: @Out Tn B C C *)
  apply (out_trivial B I);auto.
(* Goal: @Perp Tn H1 B I H1 *)
  assert_diffs;auto.
(* Goal: @Out Tn B I I *)
(* Goal: @Out Tn B C C *)
  apply (out_trivial B I);auto.
(* Goal: @Perp Tn H1 B I H1 *)
  assert_diffs;auto.
  apply (l6_6 B H2 C');auto. }
(* Goal: @CongA Tn I B H1 I B H2 *)
(* Goal: @Out Tn B H2 C *)
(* Goal: @Out Tn B H2 C *)
CongA.
(* Goal: @Cong Tn H1 I H2 I *)
(* Goal: @Le Tn H1 I B I *)
Cong.
Qed.


(** The points which are at equal distance of the two side of an angle are on the bisector. *)

Lemma perp_equality_bisector : forall A B C I H1 H2,  ~ Col A B C ->
 InAngle I A B C -> Col B H1 A -> 
 Col B H2 C -> Perp A B I H1 -> Perp B C I H2 -> Cong I H1 I H2 ->
 CongA A B I I B C.
Proof.
intros A B C I H1 H2 HNCOL HINANGLE HCOLH1 HCOLH2 HPERPH1 HPERPH2 HCONG.
(* Goal: @Out Tn B H2 C *)
destruct (not_col_efoot_not_equality A B C I H1 H2) as [HNEQH1 HNEQH2];auto.
(* Goal: @Coplanar Tn A B C I *)
(* Goal: @Out Tn B H2 C *)
 Cop.
(* Goal: @Col Tn B H2 C *)
(* Goal: @OS Tn B I H2 C *)
 Col.
(* Goal: @Col Tn B H2 C *)
(* Goal: @OS Tn B I H2 C *)
 Col.
(* Goal: @Out Tn B H2 C *)
assert(HMY : Cong H1 B H2 B /\ CongA H1 B I H2 B I /\ CongA H1 I B H2 I B).
(* Goal: and (@Cong Tn H1 B H2 B) (and (@CongA Tn H1 B I H2 B I) (@CongA Tn H1 I B H2 I B)) *)
 apply (l11_52 B H1 I B H2 I).
(* Goal: @OS Tn I B H2 C *)
(* Goal: @Out Tn B H2 C *)
{ apply (l11_16 B H1 I B H2 I).
(* Goal: @Per Tn B H1 I *)
  apply (perp_per_1 H1 B I).
(* Goal: @Perp Tn H1 B I H1 *)
  assert_diffs;auto.
  assert (Perp B H1 I H1) . ( apply (perp_col B A I H1 H1);auto;Perp;Col).
(* Goal: @Perp Tn H1 B I H1 *)
  Perp.
(* Goal: @Perp Tn H1 B I H1 *)
  assert_diffs;auto.
(* Goal: @Perp Tn H1 B I H1 *)
  assert_diffs;auto.
(* Goal: @Per Tn B H2 I *)
(* Goal: not (@eq (@Tpoint Tn) B H2) *)
(* Goal: not (@eq (@Tpoint Tn) I H2) *)
(* Goal: @Cong Tn B I B I *)
(* Goal: @Cong Tn H1 I H2 I *)
(* Goal: @Le Tn H1 I B I *)
  apply (perp_per_1 H2 B I).
(* Goal: @Perp Tn H1 B I H1 *)
  assert_diffs;auto.
(* Goal: @Perp Tn H2 B I H2 *)
(* Goal: not (@eq (@Tpoint Tn) B H2) *)
(* Goal: not (@eq (@Tpoint Tn) I H2) *)
(* Goal: @Cong Tn B I B I *)
(* Goal: @Cong Tn H1 I H2 I *)
(* Goal: @Le Tn H1 I B I *)
  assert (Perp B H2 I H2) by (apply (perp_col B C I H2 H2);auto;Perp;Col).
(* Goal: @Perp Tn H1 B I H1 *)
  Perp.
(* Goal: @Perp Tn H1 B I H1 *)
  assert_diffs;auto.
(* Goal: @Perp Tn H1 B I H1 *)
  assert_diffs;auto. }
(* Goal: @Cong Tn H1 I H2 I *)
(* Goal: @Le Tn H1 I B I *)
Cong.
(* Goal: @Cong Tn H1 I H2 I *)
(* Goal: @Le Tn H1 I B I *)
Cong.
(* Goal: @Coplanar Tn I B H1 H2 *)
(* Goal: @CongA Tn I B H1 I B H2 *)
(* Goal: @Out Tn B H2 C *)
(* Goal: @Out Tn B H2 C *)
{  assert_diffs.
(* Goal: @Le Tn H1 I B I *)
   apply (l11_46 B H1 I); auto.
(* Goal: or (@Per Tn B H1 I) (@Obtuse Tn B H1 I) *)
   left.
(* Goal: @Per Tn B H1 I *)
   apply (perp_per_1 H1 B I).
(* Goal: @Perp Tn H1 B I H1 *)
   assert_diffs;auto.
   assert (Perp B H1 I H1) by ( apply (perp_col B A I H1 H1);auto;Perp;Col).
   Perp. }
(* Goal: @Out Tn B H2 C *)
destruct HMY as [HSH1BH2B [HAH1BI HAH1IB]].
destruct (out_dec B A H1) as [HOUT | HBET].
assert (Out B H2 C) by (apply (equality_foot_out_out A B C I H1 H2);auto;Col;Col;apply (l6_6 B A H1);auto).
assert (CongA A B I C B I).
(* Goal: @OS Tn I B H2 C *)
(* Goal: @Out Tn B H2 C *)
{ apply (out_conga H1 B I H2 B I A I C I);auto.
 apply (l6_6 B A H1);auto.
(* Goal: @Out Tn B I I *)
(* Goal: @Out Tn B C C *)
 apply (out_trivial B I);auto.
(* Goal: @Perp Tn H1 B I H1 *)
 assert_diffs;auto.
(* Goal: @Out Tn B I I *)
(* Goal: @Out Tn B C C *)
 apply (out_trivial B I);auto.
(* Goal: @Perp Tn H1 B I H1 *)
 assert_diffs;auto. }
(* Goal: @CongA Tn I B H1 I B H2 *)
(* Goal: @Out Tn B H2 C *)
(* Goal: @Out Tn B H2 C *)
CongA.
assert (~ Out B C H2).
(* Goal: @OS Tn I B H2 C *)
(* Goal: @Out Tn B H2 C *)
{  intro.
   assert (Out B H1 A).
(* Goal: @OS Tn I B H2 C *)
(* Goal: @Out Tn B H2 C *)
   { apply (equality_foot_out_out C B A I H2 H1);auto.
(* Goal: not (@Col Tn B C I) *)
     intro.
     elim HNCOL;Col.
     apply (l11_24 I A B C);auto.
(* Goal: @Col Tn B H2 C *)
(* Goal: @OS Tn B I H2 C *)
     Col.
(* Goal: @Col Tn B H2 C *)
(* Goal: @OS Tn B I H2 C *)
     Col.
(* Goal: @Cong Tn H1 I H2 I *)
(* Goal: @Le Tn H1 I B I *)
     Cong.
(* Goal: @Perp Tn H1 B I H1 *)
     Perp.
(* Goal: @Perp Tn H1 B I H1 *)
     Perp.
     apply (l6_6 B C H2);auto. }
  elim HBET.
  apply (l6_6 B H1 A);auto.  }
assert (Bet A B H1) by (apply (not_out_bet A B H1);auto;Col).
assert (Bet C B H2) by (apply (not_out_bet C B H2);auto;Col).
assert (CongA A B I C B I) by (apply (l11_13 H1 B I H2 B I A C);auto;
      Between;assert_diffs;auto;Between;assert_diffs;auto).
(* Goal: @CongA Tn I B H1 I B H2 *)
(* Goal: @Out Tn B H2 C *)
(* Goal: @Out Tn B H2 C *)
CongA.
Qed.

End Bisector_2.
