Require Export GeoCoq.Tarski_dev.Ch12_parallel.
Require Export GeoCoq.Tarski_dev.Annexes.perp_bisect.

Section Triangles.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Section ABC.

Variable A B C : Tpoint.

Definition isosceles A B C :=
 Cong A B B C.

Lemma isosceles_sym :
  isosceles A B C ->
  isosceles C B A.
Proof.
(* Goal: isosceles C A B *)
unfold isosceles.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)) (_ : @CongA Tn B A C A B C) (_ : @CongA Tn A B C B C A), equilateral A B C *)
intros.
(* Goal: @Cong Tn C A A B *)
Cong.
Qed.

Lemma isosceles_conga :
  A<>C -> A<>B ->
  isosceles A B C ->
  CongA C A B A C B.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)) (_ : @CongA Tn B A C A B C) (_ : @CongA Tn A B C B C A), equilateral A B C *)
intros.
(* Goal: @CongA Tn C A B A C B *)
apply cong3_conga.
(* Goal: and (not (@Col Tn A B C)) (and (not (@eq (@Tpoint Tn) A H)) (and (not (@eq (@Tpoint Tn) C H)) (and (@Midpoint Tn H A C) (@CongA Tn H B A H B C)))) *)
auto.
(* Goal: and (not (@Col Tn A B C)) (and (not (@eq (@Tpoint Tn) A H)) (and (not (@eq (@Tpoint Tn) C H)) (and (@Midpoint Tn H A C) (@CongA Tn H B A H B C)))) *)
auto.
(* Goal: @Cong_3 Tn C A B A C B *)
unfold Cong_3.
(* Goal: and (@Cong Tn C A A C) (and (@Cong Tn C B A B) (@Cong Tn A B C B)) *)
unfold isosceles in H.
(* Goal: @Cong Tn C A A B *)
repeat split;Cong.
Qed.

Lemma conga_isosceles :
 ~ Col A B C ->
 CongA C A B A C B ->
 isosceles A B C. 
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)) (_ : @CongA Tn B A C A B C) (_ : @CongA Tn A B C B C A), equilateral A B C *)
intros.
assert (Cong B A B C)
 by (apply l11_44_1_b;finish;CongA).
(* Goal: isosceles C A B *)
unfold isosceles.
(* Goal: @Cong Tn C A A B *)
Cong.
Qed.

(** In a triangle isosceles in A the altitude wrt. A, is also the bisector and median. *)

Lemma isosceles_foot__midpoint_conga :
 forall H,
 isosceles A B C ->
 Col H A C -> 
 Perp H B A C ->
 ~ Col A B C /\ A<>H /\ C<>H /\ Midpoint H A C /\ CongA H B A H B C.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)) (_ : @CongA Tn B A C A B C) (_ : @CongA Tn A B C B C A), equilateral A B C *)
intros.
(* Goal: and (not (@Col Tn A B C)) (and (not (@eq (@Tpoint Tn) A H)) (and (not (@eq (@Tpoint Tn) C H)) (and (@Midpoint Tn H A C) (@CongA Tn H B A H B C)))) *)
assert_diffs.
(* Goal: and (not (@Col Tn A B C)) (and (not (@eq (@Tpoint Tn) A H)) (and (not (@eq (@Tpoint Tn) C H)) (and (@Midpoint Tn H A C) (@CongA Tn H B A H B C)))) *)
assert (~ Col A B C).
(* Goal: not (@eq (@Tpoint Tn) C H) *)
(* Goal: and (not (@Col Tn A B C)) (and (not (@eq (@Tpoint Tn) A H)) (and (not (@eq (@Tpoint Tn) C H)) (and (@Midpoint Tn H A C) (@CongA Tn H B A H B C)))) *)
 {
(* Goal: not (@Col Tn A B C) *)
   intro;apply perp_not_col2 in H2.
(* Goal: False *)
   destruct H2;apply H2;ColR.
 }
(* Goal: and (not (@Col Tn A B C)) (and (not (@eq (@Tpoint Tn) A H)) (and (not (@eq (@Tpoint Tn) C H)) (and (@Midpoint Tn H A C) (@CongA Tn H B A H B C)))) *)
assert_diffs. 
(* Goal: and (not (@Col Tn A B C)) (and (not (@eq (@Tpoint Tn) A H)) (and (not (@eq (@Tpoint Tn) C H)) (and (@Midpoint Tn H A C) (@CongA Tn H B A H B C)))) *)
assert (A<>H).
(* Goal: not (@eq (@Tpoint Tn) C H) *)
(* Goal: and (not (@Col Tn A B C)) (and (not (@eq (@Tpoint Tn) A H)) (and (not (@eq (@Tpoint Tn) C H)) (and (@Midpoint Tn H A C) (@CongA Tn H B A H B C)))) *)
 { (* these point are distinct 
      because otherwise the hypothenuse is not larger than the side *)
(* Goal: not (@Col Tn A B C) *)
 intro.
(* Goal: False *)
 treat_equalities.
(* Goal: False *)
 assert (Lt A B B C /\ Lt A C B C).
(* Goal: and (not (@Col Tn A B C)) (and (not (@eq (@Tpoint Tn) A H)) (and (not (@eq (@Tpoint Tn) C H)) (and (@Midpoint Tn H A C) (@CongA Tn H B A H B C)))) *)
 apply (l11_46 B A C);Col; left;apply perp_per_2;auto.
(* Goal: not (@Col Tn A B C) *)
 spliter.
(* Goal: equilateral A B C *)
 unfold isosceles in *.
(* Goal: and (not (@Col Tn A B C)) (and (not (@eq (@Tpoint Tn) A H)) (and (not (@eq (@Tpoint Tn) C H)) (and (@Midpoint Tn H A C) (@CongA Tn H B A H B C)))) *)
 apply (cong__nlt A B B C);auto.
 }
(* Goal: and (not (@Col Tn A B C)) (and (not (@eq (@Tpoint Tn) A H)) (and (not (@eq (@Tpoint Tn) C H)) (and (@Midpoint Tn H A C) (@CongA Tn H B A H B C)))) *)
assert (C<>H).
(* Goal: not (@eq (@Tpoint Tn) C H) *)
(* Goal: and (not (@Col Tn A B C)) (and (not (@eq (@Tpoint Tn) A H)) (and (not (@eq (@Tpoint Tn) C H)) (and (@Midpoint Tn H A C) (@CongA Tn H B A H B C)))) *)
 {
(* Goal: not (@Col Tn A B C) *)
 intro.
(* Goal: False *)
 treat_equalities.
(* Goal: False *)
 assert (Lt C B B A /\ Lt C A B A).
(* Goal: and (@Lt Tn C B B A) (@Lt Tn C A B A) *)
(* Goal: False *)
 apply (l11_46 B C A);Col; left;apply perp_per_2;finish.
(* Goal: not (@Col Tn A B C) *)
 spliter.
(* Goal: equilateral A B C *)
 unfold isosceles in *.
(* Goal: False *)
 apply (cong__nlt C B B A);finish.
 } 
assert (Perp_at H A C B H)
 by (apply l8_14_2_1b_bis;finish).
(* Goal: and (not (@Col Tn A B C)) (and (not (@eq (@Tpoint Tn) A H)) (and (not (@eq (@Tpoint Tn) C H)) (and (@Midpoint Tn H A C) (@CongA Tn H B A H B C)))) *)
assert (Per A H B) by (apply perp_in_per_1 with C H;finish).
(* Goal: and (not (@Col Tn A B C)) (and (not (@eq (@Tpoint Tn) A H)) (and (not (@eq (@Tpoint Tn) C H)) (and (@Midpoint Tn H A C) (@CongA Tn H B A H B C)))) *)
assert (Per C H B) by (apply perp_in_per_3 with A H;finish). 
(* We prove that A H B and C H B are congruent triangles *)
assert (Cong H A H C /\ CongA H A B H C B /\ CongA H B A H B C)
 by (apply (cong2_per2__cong_conga2 A H B C H B);finish).
(* Goal: not (@Col Tn A B C) *)
spliter.
assert (Midpoint H A C)
 by (apply l7_20_bis;finish).
(* Goal: and (not (@Col Tn A B C)) (and (not (@eq (@Tpoint Tn) A H)) (and (not (@eq (@Tpoint Tn) C H)) (and (@Midpoint Tn H A C) (@CongA Tn H B A H B C)))) *)
auto.
Qed.

Definition equilateral A B C :=
 Cong A B B C /\ Cong B C C A.

Definition equilateral_strict A B C :=
 equilateral A B C /\ A <> B.

Lemma equilateral_strict_equilateral :
 equilateral_strict A B C ->
 equilateral A B C.
Proof.
(* Goal: and (not (@Col Tn A B C)) (and (not (@eq (@Tpoint Tn) A H)) (and (not (@eq (@Tpoint Tn) C H)) (and (@Midpoint Tn H A C) (@CongA Tn H B A H B C)))) *)
unfold equilateral_strict in *. tauto.
Qed.

Lemma equilateral_cong:
  equilateral A B C ->
  Cong A B B C /\ Cong B C C A /\ Cong C A A B.
Proof.
(* Goal: @Cong Tn C A A B *)
unfold equilateral;intros;intuition Cong.
(* Goal: @Cong Tn C A A B *)
assert (T:=cong_transitivity A B B C C A H0 H1).
(* Goal: @Cong Tn C A A B *)
Cong.
Qed.

Lemma equilateral_rot :
 equilateral A B C ->
 equilateral B C A.
Proof.
(* Goal: not (@Col Tn A B C) *)
intro.
(* Goal: isosceles C A B *)
apply equilateral_cong in H.
(* Goal: equilateral A B C *)
unfold equilateral.
(* Goal: @Cong Tn C A A B *)
intuition Cong.
Qed.

Lemma equilateral_swap :
 equilateral A B C ->
 equilateral B A C.
Proof.
(* Goal: not (@Col Tn A B C) *)
intro.
(* Goal: isosceles C A B *)
apply equilateral_cong in H.
(* Goal: equilateral A B C *)
unfold equilateral.
(* Goal: @Cong Tn C A A B *)
intuition Cong.
Qed.

Lemma equilateral_rot_2 :
 equilateral A B C ->
 equilateral C B A.
Proof.
(* Goal: not (@Col Tn A B C) *)
intro.
(* Goal: isosceles C A B *)
apply equilateral_cong in H.
(* Goal: equilateral A B C *)
unfold equilateral.
(* Goal: @Cong Tn C A A B *)
intuition Cong.
Qed.

Lemma equilateral_swap_2 :
 equilateral A B C ->
 equilateral A C B.
Proof.
(* Goal: not (@Col Tn A B C) *)
intro.
(* Goal: isosceles C A B *)
apply equilateral_cong in H.
(* Goal: equilateral A B C *)
unfold equilateral.
(* Goal: @Cong Tn C A A B *)
intuition Cong.
Qed.

Lemma equilateral_swap_rot :
 equilateral A B C ->
 equilateral C A B.
Proof.
(* Goal: not (@Col Tn A B C) *)
intro.
(* Goal: isosceles C A B *)
apply equilateral_cong in H.
(* Goal: equilateral A B C *)
unfold equilateral.
(* Goal: @Cong Tn C A A B *)
intuition Cong.
Qed.

Hint Resolve equilateral_swap equilateral_swap_2
 equilateral_swap_rot equilateral_rot equilateral_rot_2 : equilateral.

Lemma equilateral_isosceles_1 :
  equilateral A B C ->
  isosceles A B C.
Proof.
(* Goal: forall _ : equilateral A B C, isosceles B C A *)
unfold equilateral, isosceles.
(* Goal: and (not (@Col Tn A B C)) (and (not (@eq (@Tpoint Tn) A H)) (and (not (@eq (@Tpoint Tn) C H)) (and (@Midpoint Tn H A C) (@CongA Tn H B A H B C)))) *)
tauto.
Qed.

Lemma equilateral_isosceles_2 :
  equilateral A B C ->
  isosceles B C A.
Proof.
(* Goal: forall _ : equilateral A B C, isosceles B C A *)
unfold equilateral, isosceles.
(* Goal: and (not (@Col Tn A B C)) (and (not (@eq (@Tpoint Tn) A H)) (and (not (@eq (@Tpoint Tn) C H)) (and (@Midpoint Tn H A C) (@CongA Tn H B A H B C)))) *)
tauto.
Qed.

Lemma equilateral_isosceles_3 :
  equilateral A B C ->
  isosceles C A B.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)) (_ : @CongA Tn B A C A B C) (_ : @CongA Tn A B C B C A), equilateral A B C *)
intros.
(* Goal: isosceles C A B *)
apply equilateral_cong in H.
(* Goal: isosceles C A B *)
unfold isosceles.
(* Goal: and (not (@Col Tn A B C)) (and (not (@eq (@Tpoint Tn) A H)) (and (not (@eq (@Tpoint Tn) C H)) (and (@Midpoint Tn H A C) (@CongA Tn H B A H B C)))) *)
tauto.
Qed.

Hint Resolve equilateral_isosceles_1 equilateral_isosceles_2 equilateral_isosceles_3 : equilateral.

Lemma equilateral_strict_neq :
 equilateral_strict A B C ->
 A <> B /\ B <> C /\ A <> C.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)) (_ : @CongA Tn B A C A B C) (_ : @CongA Tn A B C B C A), equilateral A B C *)
intros.
unfold equilateral_strict, equilateral in H.
decompose [and] H;clear H.
(* Goal: @Cong Tn C A A B *)
repeat split;Cong.
eauto using cong_diff.
eapply cong_diff.
assert (T:=cong_transitivity A B B C C A H2 H3).
apply H1.
assert (T:=cong_transitivity A B B C C A H2 H3).
(* Goal: @Cong Tn C A A B *)
Cong.
Qed.

Hint Resolve equilateral_strict_neq : equilateral.

Lemma equilateral_strict_swap_1 :
 equilateral_strict A B C ->
 equilateral_strict A C B.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)) (_ : @CongA Tn B A C A B C) (_ : @CongA Tn A B C B C A), equilateral A B C *)
intros.
(* Goal: @CongA Tn C A B A C B *)
assert (T:= equilateral_strict_neq H).
(* Goal: not (@Col Tn A B C) *)
unfold equilateral_strict in *.
(* Goal: and (equilateral C B A) (not (@eq (@Tpoint Tn) C B)) *)
intuition (eauto with equilateral).
Qed.

Lemma equilateral_strict_swap_2 :
 equilateral_strict A B C ->
 equilateral_strict B A C.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)) (_ : @CongA Tn B A C A B C) (_ : @CongA Tn A B C B C A), equilateral A B C *)
intros.
(* Goal: @CongA Tn C A B A C B *)
assert (T:= equilateral_strict_neq H).
(* Goal: not (@Col Tn A B C) *)
unfold equilateral_strict in *.
(* Goal: and (equilateral C B A) (not (@eq (@Tpoint Tn) C B)) *)
intuition (eauto with equilateral).
Qed.

Lemma equilateral_strict_swap_3 :
 equilateral_strict A B C ->
 equilateral_strict B C A.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)) (_ : @CongA Tn B A C A B C) (_ : @CongA Tn A B C B C A), equilateral A B C *)
intros.
(* Goal: @CongA Tn C A B A C B *)
assert (T:= equilateral_strict_neq H).
(* Goal: not (@Col Tn A B C) *)
unfold equilateral_strict in *.
(* Goal: and (equilateral C B A) (not (@eq (@Tpoint Tn) C B)) *)
intuition (eauto with equilateral).
Qed.

Lemma equilateral_strict_swap_4 :
 equilateral_strict A B C ->
 equilateral_strict C A B.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)) (_ : @CongA Tn B A C A B C) (_ : @CongA Tn A B C B C A), equilateral A B C *)
intros.
(* Goal: @CongA Tn C A B A C B *)
assert (T:= equilateral_strict_neq H).
(* Goal: not (@Col Tn A B C) *)
unfold equilateral_strict in *.
(* Goal: and (equilateral C B A) (not (@eq (@Tpoint Tn) C B)) *)
intuition (eauto with equilateral).
Qed.

Lemma equilateral_strict_swap_5 :
 equilateral_strict A B C ->
 equilateral_strict C B A.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)) (_ : @CongA Tn B A C A B C) (_ : @CongA Tn A B C B C A), equilateral A B C *)
intros.
(* Goal: @CongA Tn C A B A C B *)
assert (T:= equilateral_strict_neq H).
(* Goal: not (@Col Tn A B C) *)
unfold equilateral_strict in *.
(* Goal: and (equilateral C B A) (not (@eq (@Tpoint Tn) C B)) *)
intuition (eauto with equilateral).
Qed.

Hint Resolve equilateral_strict_swap_1 equilateral_strict_swap_2
equilateral_strict_swap_3 equilateral_strict_swap_4 equilateral_strict_swap_5 : equilateral.

Lemma equilateral_strict__not_col : 
 equilateral_strict A B C -> ~ Col A B C.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)) (_ : @CongA Tn B A C A B C) (_ : @CongA Tn A B C B C A), equilateral A B C *)
intros.
(* Goal: @CongA Tn C A B A C B *)
assert (T:=(equilateral_strict_neq H)).
(* Goal: not (@Col Tn A B C) *)
unfold equilateral_strict in *.
(* Goal: not (@Col Tn A B C) *)
unfold equilateral in *.
(* Goal: not (@Col Tn A B C) *)
spliter.
(* Goal: not (@Col Tn A B C) *)
intro.
(* Goal: False *)
assert (Midpoint B A C) by (apply (l7_20_bis B A C);finish).
(* Goal: False *)
assert (Midpoint C A B) by (apply (l7_20_bis C A B);finish).
(* Goal: and (not (@Col Tn A B C)) (and (not (@eq (@Tpoint Tn) A H)) (and (not (@eq (@Tpoint Tn) C H)) (and (@Midpoint Tn H A C) (@CongA Tn H B A H B C)))) *)
apply midpoint_not_midpoint with C A B;auto.
Qed.

Lemma equilateral_strict_conga_1 :
 equilateral_strict A B C ->
 CongA C A B A C B.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)) (_ : @CongA Tn B A C A B C) (_ : @CongA Tn A B C B C A), equilateral A B C *)
intros.
(* Goal: @CongA Tn C A B A C B *)
assert (T:= equilateral_strict_neq H).
(* Goal: @CongA Tn C A B A C B *)
apply equilateral_strict_equilateral in H.
(* Goal: @CongA Tn C A B A C B *)
apply equilateral_isosceles_1 in H.
(* Goal: @CongA Tn C A B A C B *)
apply isosceles_conga.
(* Goal: and (not (@Col Tn A B C)) (and (not (@eq (@Tpoint Tn) A H)) (and (not (@eq (@Tpoint Tn) C H)) (and (@Midpoint Tn H A C) (@CongA Tn H B A H B C)))) *)
tauto.
(* Goal: and (not (@Col Tn A B C)) (and (not (@eq (@Tpoint Tn) A H)) (and (not (@eq (@Tpoint Tn) C H)) (and (@Midpoint Tn H A C) (@CongA Tn H B A H B C)))) *)
tauto.
(* Goal: @CongA Tn C B A B C A *)
assumption.
Qed.

End ABC.

Lemma equilateral_strict_conga_2 :
 forall A B C,
 equilateral_strict A B C ->
 CongA B A C A B C.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)) (_ : @CongA Tn B A C A B C) (_ : @CongA Tn A B C B C A), equilateral A B C *)
intros.
(* Goal: @CongA Tn B A C A B C *)
apply equilateral_strict_swap_1 in H.
(* Goal: @CongA Tn C B A B C A *)
apply equilateral_strict_conga_1 in H.
(* Goal: @CongA Tn C B A B C A *)
assumption.
Qed.

Lemma equilateral_strict_conga_3 :
 forall A B C,
 equilateral_strict A B C ->
 CongA C B A B C A.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)) (_ : @CongA Tn B A C A B C) (_ : @CongA Tn A B C B C A), equilateral A B C *)
intros.
(* Goal: @CongA Tn C B A B C A *)
apply equilateral_strict_swap_2 in H.
(* Goal: @CongA Tn C B A B C A *)
apply equilateral_strict_conga_1 in H.
(* Goal: @CongA Tn C B A B C A *)
assumption.
Qed.

Lemma conga3_equilateral :
 forall A B C, 
 ~ Col A B C ->
 CongA B A C A B C ->
 CongA A B C B C A ->
 equilateral A B C.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)) (_ : @CongA Tn B A C A B C) (_ : @CongA Tn A B C B C A), equilateral A B C *)
intros.
assert (isosceles B C A)
 by (apply conga_isosceles;CongA;Col).
assert (isosceles C A B)
 by (apply conga_isosceles;CongA;Col).
(* Goal: equilateral A B C *)
unfold isosceles in *.
(* Goal: equilateral A B C *)
unfold equilateral.
(* Goal: @Cong Tn C A A B *)
split;eCong.
Qed.



End Triangles.