 (* Gabriel Braun April 2013 *)

Require Export GeoCoq.Tarski_dev.Ch13_2_length.

Section Angles_1.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

(************************************* angle *****************************)

Lemma ang_exists : forall A B C, A <> B -> C <> B -> exists a, Q_CongA a /\ a A B C.
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: @ex (forall (_ : @Tpoint Tn) (_ : @Tpoint Tn) (_ : @Tpoint Tn), Prop) (fun a : forall (_ : @Tpoint Tn) (_ : @Tpoint Tn) (_ : @Tpoint Tn), Prop => and (@Q_CongA_Acute Tn a) (a A B C)) *)
    exists (fun D E F => CongA A B C D E F).
(* Goal: iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    split.
(* Goal: @Q_CongA Tn a *)
(* Goal: a X Y Z *)
(* Goal: a X Y Z *)
(* Goal: forall _ : a X Y Z, @CongA Tn A B C X Y Z *)
      unfold Q_CongA.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Acute Tn A B C) (forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z))))) *)
      exists A.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Acute Tn A B C) (forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z)))) *)
      exists B.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Acute Tn A B C) (forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z))) *)
      exists C.
(* Goal: @Ang Tn X Y Z a *)
      split; auto.
(* Goal: @Ang Tn X Y Z a *)
      split; auto.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
      intros.
(* Goal: iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
      split.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
        auto.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      auto.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
    apply conga_refl; auto.
Qed.

Lemma ex_points_ang : forall a , Q_CongA a ->  exists A, exists B, exists C, a A B C.
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: False *)
    unfold Q_CongA in H.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Ang Tn A B C a1) (@Ang Tn A B C a2)))) *)
    ex_and H A.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Ang Tn A B C a1) (@Ang Tn A B C a2)))) *)
    ex_and H0 B.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Ang Tn A B C a1) (@Ang Tn A B C a2)))) *)
    ex_and H C.
(* Goal: @Q_CongA_Acute Tn b *)
    assert(HH:= H1 A B C).
(* Goal: @CongA Tn A B C X Y Z *)
    destruct HH.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Acute Tn A B C) (forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z))))) *)
    exists A.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Acute Tn A B C) (forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z)))) *)
    exists B.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Acute Tn A B C) (forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z))) *)
    exists C.
(* Goal: a A B C *)
    apply H2.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
    apply conga_refl; auto.
Qed.

End Angles_1.

Ltac ang_instance a A B C :=
  assert(tempo_ang:= ex_points_ang a);
  match goal with
    |H: Q_CongA a |-  _ => assert(tempo_H:=H); apply tempo_ang in tempo_H;
                       elim tempo_H; intros A ; let tempo_HP := fresh "tempo_HP" in intro tempo_HP; clear tempo_H;
                       elim tempo_HP; intro B; let tempo_HQ := fresh "tempo_HQ" in intro tempo_HQ ; clear tempo_HP ;
                       elim tempo_HQ; intro C; intro;  clear tempo_HQ
  end;
  clear tempo_ang.

Section Angles_2.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma ang_conga : forall a A B C A' B' C', Q_CongA a -> a A B C -> a A' B' C' -> CongA A B C A' B' C'.
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: False *)
    unfold Q_CongA in H.
(* Goal: not (@Bet Tn A B C) *)
    ex_and H A0.
(* Goal: a A B A *)
    ex_and H2 B0.
(* Goal: not (@Bet Tn A B C) *)
    ex_and H C0.
(* Goal: and (a A B C) (not (@Bet Tn A B C)) *)
(* Goal: forall _ : and (@Q_CongA Tn a) (@ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (a A B C) (not (@Bet Tn A B C)))))), @Q_CongA_nFlat Tn a *)
    assert(HH:=H3 A B C).
    assert(HH1:= H3 A' B' C').
(* Goal: @CongA Tn A B C X Y Z *)
    destruct HH.
    destruct HH1.
    apply H5 in H0.
    apply H7 in H1.
    eapply conga_trans.
(* Goal: @CongA Tn A B C A0 B0 C0 *)
      apply conga_sym.
(* Goal: iff (a X Y Z) (b X Y Z) *)
      apply H0.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
    auto.
Qed.

Lemma is_ang_conga : forall A B C A' B' C' a, Ang A B C a -> Ang A' B' C' a -> CongA A B C A' B' C'.
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: False *)
    unfold Ang in *.
(* Goal: b X Y Z *)
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
    spliter.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
    eapply (ang_conga a); auto.
Qed.

Lemma is_ang_conga_is_ang : forall A B C A' B' C' a, Ang A B C a -> CongA A B C A' B' C' -> Ang A' B' C' a.
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: False *)
    unfold Ang in *.
(* Goal: b X Y Z *)
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
    spliter.
(* Goal: iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    split.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      auto.
(* Goal: False *)
    unfold Q_CongA in H.
(* Goal: not (@Bet Tn A B C) *)
    ex_and H A0.
(* Goal: a A B A *)
    ex_and H2 B0.
(* Goal: not (@Bet Tn A B C) *)
    ex_and H C0.
(* Goal: and (a A B C) (not (@Bet Tn A B C)) *)
(* Goal: forall _ : and (@Q_CongA Tn a) (@ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (a A B C) (not (@Bet Tn A B C)))))), @Q_CongA_nFlat Tn a *)
    assert(HH:= H3 A B C).
(* Goal: @CongA Tn A B C X Y Z *)
    destruct HH.
    assert(HH1:= H3 A' B' C').
    destruct HH1.
    apply H5 in H1.
(* Goal: @CongA Tn A0 B0 C0 A B C *)
(* Goal: a A' B C' *)
    apply H6.
    eapply conga_trans.
(* Goal: False *)
      apply H1.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
    auto.
Qed.

Lemma not_conga_not_ang : forall A B C A' B' C' a , Q_CongA a -> ~(CongA A B C A' B' C') -> a A B C -> ~(a A' B' C').
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
    intro.
(* Goal: False *)
    assert(HH:=ang_conga a A B C A' B' C' H H1 H2).
(* Goal: @Out Tn B A C *)
(* Goal: @Out Tn B A C *)
(* Goal: and (@Out Tn B A C) (@Q_CongA_Null_Acute Tn a) *)
    contradiction.
Qed.

Lemma not_conga_is_ang : forall A B C A' B' C' a , ~(CongA A B C A' B' C') -> Ang A B C a -> ~(a A' B' C').
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: not (a A' B' C') *)
    unfold Ang in H0.
(* Goal: b X Y Z *)
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
    spliter.
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
    intro.
(* Goal: False *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (a A B C) (@OS Tn A B C P)) *)
    apply H.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
    apply (ang_conga a); auto.
Qed.

Lemma not_cong_is_ang1 : forall A B C A' B' C' a , ~(CongA A B C A' B' C') -> Ang A B C a -> ~(Ang A' B' C' a).
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
    intro.
(* Goal: False *)
    unfold Ang in *.
(* Goal: b X Y Z *)
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
    spliter.
(* Goal: False *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (a A B C) (@OS Tn A B C P)) *)
    apply H.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
    apply (ang_conga a); auto.
Qed.

Lemma ex_eqa : forall a1 a2, (exists A , exists B, exists C, Ang A B C a1 /\ Ang A B C a2)  -> EqA a1 a2.
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Ang Tn A B C a1) (@Ang Tn A B C a2)))) *)
    ex_and H A.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Ang Tn A B C a1) (@Ang Tn A B C a2)))) *)
    ex_and H0 B.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Ang Tn A B C a1) (@Ang Tn A B C a2)))) *)
    ex_and H C.
(* Goal: a A' B C' *)
    assert(HH:=H).
(* Goal: @EqA Tn a1 a2 *)
    assert(HH0:=H0).
(* Goal: @EqA Tn a1 a2 *)
    unfold Ang in HH.
(* Goal: @EqA Tn a1 a2 *)
    unfold Ang in HH0.
(* Goal: b X Y Z *)
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
    spliter.
(* Goal: @EqA Tn x x *)
(* Goal: @Symmetric (forall (_ : @Tpoint Tn) (_ : @Tpoint Tn) (_ : @Tpoint Tn), Prop) (@EqA Tn) *)
(* Goal: @Transitive (forall (_ : @Tpoint Tn) (_ : @Tpoint Tn) (_ : @Tpoint Tn), Prop) (@EqA Tn) *)
    unfold EqA.
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
    repeat split; auto; intro.
(* Goal: @Out Tn B0 A0 C0 *)
      assert(CongA A B C A0 B0 C0).
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
        eapply (is_ang_conga _ _ _ _ _ _ a1); auto.
(* Goal: @Ang Tn X Y Z a *)
        split; auto.
(* Goal: a2 A0 B0 C0 *)
(* Goal: a1 A0 B0 C0 *)
      assert(Ang A0 B0 C0 a2).
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
        apply (is_ang_conga_is_ang A B C); auto.
(* Goal: a1 A0 B0 C0 *)
      unfold Ang in H7.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      tauto.
(* Goal: @Out Tn B0 A0 C0 *)
    assert(CongA A B C A0 B0 C0).
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      eapply (is_ang_conga _ _ _ _ _ _ a2); auto.
(* Goal: @Ang Tn X Y Z a *)
      split; auto.
(* Goal: a1 A0 B0 C0 *)
    assert(Ang A0 B0 C0 a1).
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      apply (is_ang_conga_is_ang A B C); auto.
(* Goal: a1 A0 B0 C0 *)
    unfold Ang in H7.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
    tauto.
Qed.

Lemma all_eqa : forall A B C a1 a2, Ang A B C a1 -> Ang A B C a2 -> EqA a1 a2.
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: @EqA Tn a1 a2 *)
    apply ex_eqa.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Acute Tn A B C) (forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z))))) *)
    exists A.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Acute Tn A B C) (forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z)))) *)
    exists B.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Acute Tn A B C) (forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z))) *)
    exists C.
(* Goal: @Ang Tn X Y Z a *)
    split; auto.
Qed.

Lemma is_ang_distinct : forall A B C a , Ang A B C a -> A <> B /\ C <> B.
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) C B)) *)
    unfold Ang in H.
(* Goal: b X Y Z *)
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
    spliter.
(* Goal: False *)
    unfold Q_CongA in H.
(* Goal: not (@Bet Tn A B C) *)
    ex_and H A0.
(* Goal: not (@Bet Tn A B C) *)
    ex_and H1 B0.
(* Goal: not (@Bet Tn A B C) *)
    ex_and H C0.
(* Goal: @Out Tn B A C *)
    assert(HH:= H2 A B C).
(* Goal: @CongA Tn A B C X Y Z *)
    destruct HH.
(* Goal: a C B A *)
    apply H4 in H0.
(* Goal: and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) C B)) *)
    unfold CongA in H0.
(* Goal: b X Y Z *)
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
    spliter.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
    tauto.
Qed.


Lemma null_ang : forall A B C D a1 a2, Ang A B A a1 -> Ang C D C a2 -> EqA a1 a2.
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: @EqA Tn a1 a2 *)
    eapply (all_eqa A B A).
(* Goal: False *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (a A B C) (@OS Tn A B C P)) *)
      apply H.
(* Goal: @Ang Tn A B A a2 *)
    eapply (is_ang_conga_is_ang C D C).
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      auto.
(* Goal: @CongA Tn C D C A B A *)
    eapply l11_21_b.
(* Goal: @Out Tn B A A *)
      apply out_trivial.
(* Goal: not (@eq (@Tpoint Tn) C D) *)
(* Goal: @Out Tn B A A *)
      apply is_ang_distinct in H0.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      tauto.
(* Goal: @Out Tn B A A *)
    apply out_trivial.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
    apply is_ang_distinct in H.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
    tauto.
Qed.

Lemma flat_ang : forall A B C A' B' C' a1 a2, Bet A B C -> Bet A' B' C' -> Ang A B C a1 -> Ang A' B' C' a2  -> EqA a1 a2.
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: @EqA Tn a1 a2 *)
    eapply (all_eqa A B C).
(* Goal: False *)
      apply H1.
(* Goal: @Ang Tn A B C a2 *)
    eapply (is_ang_conga_is_ang A' B' C').
(* Goal: a A B C *)
      apply H2.
(* Goal: @CongA Tn A' B' C' A B C *)
    apply is_ang_distinct in H1.
(* Goal: @CongA Tn A' B' C' A B C *)
    apply is_ang_distinct in H2.
(* Goal: b X Y Z *)
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
    spliter.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
    eapply conga_line; auto.
Qed.

Lemma ang_distinct: forall a A B C, Q_CongA a -> a A B C -> A <> B /\ C <> B.
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: a A' B' C' *)
    assert(Ang A B C a).
(* Goal: @Ang Tn X Y Z a *)
      split; auto.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
    apply (is_ang_distinct _ _ _ a); auto.
Qed.

Lemma ex_ang : forall A B C, B <> A -> B <> C -> exists a, Q_CongA a /\ a A B C.
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: @ex (forall (_ : @Tpoint Tn) (_ : @Tpoint Tn) (_ : @Tpoint Tn), Prop) (fun a : forall (_ : @Tpoint Tn) (_ : @Tpoint Tn) (_ : @Tpoint Tn), Prop => and (@Q_CongA_Acute Tn a) (a A B C)) *)
    exists (fun X Y Z => CongA A B C X Y Z).
(* Goal: @Q_CongA Tn a *)
(* Goal: a X Y Z *)
(* Goal: a X Y Z *)
(* Goal: forall _ : a X Y Z, @CongA Tn A B C X Y Z *)
    unfold Q_CongA.
(* Goal: iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    split.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Acute Tn A B C) (forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z))))) *)
      exists A.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Acute Tn A B C) (forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z)))) *)
      exists B.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Acute Tn A B C) (forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z))) *)
      exists C.
(* Goal: iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
      split.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
        auto.
(* Goal: iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
      split.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
        auto.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
      intros.
(* Goal: iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
      split.
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
        intro.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
        auto.
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
      intro.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      auto.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
    apply conga_refl; auto.
Qed.

(************************************* Acute angle *****************************************)

Lemma anga_exists : forall A B C, A <> B -> C <> B -> Acute A B C -> exists a, Q_CongA_Acute a /\ a A B C.
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: @ex (forall (_ : @Tpoint Tn) (_ : @Tpoint Tn) (_ : @Tpoint Tn), Prop) (fun a : forall (_ : @Tpoint Tn) (_ : @Tpoint Tn) (_ : @Tpoint Tn), Prop => and (@Q_CongA_Acute Tn a) (a A B C)) *)
    exists (fun D E F => CongA A B C D E F).
(* Goal: iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    split.
(* Goal: @Q_CongA Tn a *)
(* Goal: a X Y Z *)
(* Goal: a X Y Z *)
(* Goal: forall _ : a X Y Z, @CongA Tn A B C X Y Z *)
      unfold Q_CongA.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Acute Tn A B C) (forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z))))) *)
      exists A.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Acute Tn A B C) (forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z)))) *)
      exists B.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Acute Tn A B C) (forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z))) *)
      exists C.
(* Goal: iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
      split.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
        auto.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
      intros.
(* Goal: @Ang Tn X Y Z a *)
      split; auto.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
    apply conga_refl; auto.
Qed.

Lemma anga_is_ang : forall a, Q_CongA_Acute a -> Q_CongA a.
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: @Acute Tn A B C *)
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    unfold Q_CongA_Acute in H.
(* Goal: @Q_CongA Tn a *)
(* Goal: a X Y Z *)
(* Goal: a X Y Z *)
(* Goal: forall _ : a X Y Z, @CongA Tn A B C X Y Z *)
    unfold Q_CongA.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Ang Tn A B C a1) (@Ang Tn A B C a2)))) *)
    ex_and H A.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Ang Tn A B C a1) (@Ang Tn A B C a2)))) *)
    ex_and H0 B.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Ang Tn A B C a1) (@Ang Tn A B C a2)))) *)
    ex_and H C.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Acute Tn A B C) (forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z))))) *)
    exists A.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Acute Tn A B C) (forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z)))) *)
    exists B.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Acute Tn A B C) (forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z))) *)
    exists C.
(* Goal: and (not (@eq (@Tpoint Tn) A0 B0)) (and (not (@eq (@Tpoint Tn) C0 B0)) (and (not (@eq (@Tpoint Tn) C0 B0)) (@ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn A0 X C0) (or (@eq (@Tpoint Tn) X B0) (@Out Tn B0 X C0)))))) *)
(* Goal: @CongA Tn A B C A0 B0 C0 *)
    apply acute_distincts in H.
(* Goal: b X Y Z *)
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
    spliter.
(* Goal: iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    split.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      auto.
(* Goal: iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    split.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      auto.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    split.
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
      intro.
(* Goal: b X Y Z *)
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
      assert(Ang X Y Z a).
(* Goal: @Ang Tn A B C a *)
(* Goal: a A' B' C' *)
        unfold Ang.
(* Goal: iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
        split.
(* Goal: @Q_CongA Tn a *)
(* Goal: a X Y Z *)
(* Goal: a X Y Z *)
(* Goal: forall _ : a X Y Z, @CongA Tn A B C X Y Z *)
          unfold Q_CongA.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Acute Tn A B C) (forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z))))) *)
          exists A.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Acute Tn A B C) (forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z)))) *)
          exists B.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Acute Tn A B C) (forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z))) *)
          exists C.
(* Goal: iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
          split.
(* Goal: not (@eq (@Tpoint Tn) x1 x0) *)
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn x x0 x1 X Y Z) (b X Y Z) *)
            assumption.
(* Goal: iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
          split.
(* Goal: not (@eq (@Tpoint Tn) x1 x0) *)
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn x x0 x1 X Y Z) (b X Y Z) *)
            assumption.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
          auto.
(* Goal: a X Y Z *)
(* Goal: a X Y Z *)
(* Goal: forall _ : a X Y Z, @CongA Tn A B C X Y Z *)
        assert(HH:= H0 X Y Z).
(* Goal: and (not (@eq (@Tpoint Tn) A' B')) (not (@eq (@Tpoint Tn) C' B')) *)
(* Goal: @InAngle Tn C' A' B' C' *)
(* Goal: @CongA Tn A B C A' B' C' *)
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
        apply HH.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
        auto.
(* Goal: a A' B' C' *)
      unfold Ang in H3.
(* Goal: b X Y Z *)
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
      spliter.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      auto.
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
    intro.
(* Goal: iff (a X Y Z) (b X Y Z) *)
    apply H0.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
    auto.
Qed.

Lemma ex_points_anga : forall a , Q_CongA_Acute a ->  exists A, exists B, exists C, a A B C.
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: a A' B C' *)
    assert(HH:=H).
(* Goal: @Q_CongA Tn a *)
(* Goal: forall (A B C : @Tpoint Tn) (_ : a A B C), not (@Bet Tn A B C) *)
    apply anga_is_ang in H.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => a A B C))) *)
    ang_instance a A B C.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Acute Tn A B C) (forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z))))) *)
    exists A.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Acute Tn A B C) (forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z)))) *)
    exists B.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Acute Tn A B C) (forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z))) *)
    exists C.
(* Goal: not (@eq (@Tpoint Tn) x1 x0) *)
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn x x0 x1 X Y Z) (b X Y Z) *)
    assumption.
Qed.

End Angles_2.

Ltac anga_instance a A B C :=
  assert(tempo_anga:= ex_points_anga a);
  match goal with
    |H: Q_CongA_Acute a |-  _ => assert(tempo_H:=H); apply tempo_anga in tempo_H;
                                 elim tempo_H; intros A ;
                                 let tempo_HP := fresh "tempo_HP" in
                                 intro tempo_HP; clear tempo_H;
                                 elim tempo_HP; intro B;
                                 let tempo_HQ := fresh "tempo_HQ" in
                                 intro tempo_HQ ; clear tempo_HP ;
                        elim tempo_HQ; intro C; intro;  clear tempo_HQ
  end;
  clear tempo_anga.

Require Import Setoid.

Section Angles_3.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma anga_conga : forall a A B C A' B' C', Q_CongA_Acute a -> a A B C -> a A' B' C' -> CongA A B C A' B' C'.
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
    apply (ang_conga a); auto.
(* Goal: @Q_CongA Tn a *)
(* Goal: a A B C *)
    apply anga_is_ang.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
    auto.
Qed.

Lemma is_anga_to_is_ang : forall A B C a, Ang_Acute A B C a -> Ang A B C a.
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: @Ang Tn A B C a *)
    unfold Ang_Acute in H.
(* Goal: @Ang Tn A B C a *)
(* Goal: a A' B' C' *)
    unfold Ang.
(* Goal: b X Y Z *)
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
    spliter.
(* Goal: iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    split.
(* Goal: @Q_CongA Tn a *)
(* Goal: a A B C *)
      apply anga_is_ang.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      auto.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
    auto.
Qed.

Lemma is_anga_conga : forall A B C A' B' C' a, Ang_Acute A B C a -> Ang_Acute A' B' C' a -> CongA A B C A' B' C'.
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: False *)
    unfold Ang_Acute in *.
(* Goal: b X Y Z *)
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
    spliter.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
    apply (anga_conga a); auto.
Qed.

Lemma is_anga_conga_is_anga : forall A B C A' B' C' a, Ang_Acute A B C a -> CongA A B C A' B' C' -> Ang_Acute A' B' C' a.
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: False *)
    unfold Ang_Acute in *.
(* Goal: b X Y Z *)
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
    spliter.
(* Goal: iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    split.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      auto.
(* Goal: @Q_CongA Tn a *)
(* Goal: forall (A B C : @Tpoint Tn) (_ : a A B C), not (@Bet Tn A B C) *)
    apply anga_is_ang in H.
(* Goal: False *)
    unfold Q_CongA in H.
(* Goal: not (@Bet Tn A B C) *)
    ex_and H A0.
(* Goal: a A B A *)
    ex_and H2 B0.
(* Goal: not (@Bet Tn A B C) *)
    ex_and H C0.
(* Goal: and (a A B C) (not (@Bet Tn A B C)) *)
(* Goal: forall _ : and (@Q_CongA Tn a) (@ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (a A B C) (not (@Bet Tn A B C)))))), @Q_CongA_nFlat Tn a *)
    assert(HH:= H3 A B C).
(* Goal: @CongA Tn A B C X Y Z *)
    destruct HH.
    assert(HH1:= H3 A' B' C').
    destruct HH1.
    apply H5 in H1.
(* Goal: @CongA Tn A0 B0 C0 A B C *)
(* Goal: a A' B C' *)
    apply H6.
    eapply conga_trans.
(* Goal: False *)
      apply H1.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
    auto.
Qed.

Lemma not_conga_is_anga : forall A B C A' B' C' a , ~ CongA A B C A' B' C' -> Ang_Acute A B C a -> ~(a A' B' C').
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: not (a A' B' C') *)
    unfold Ang_Acute in H0.
(* Goal: b X Y Z *)
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
    spliter.
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
    intro.
(* Goal: False *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (a A B C) (@OS Tn A B C P)) *)
    apply H.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
    apply (anga_conga a); auto.
Qed.

Lemma not_cong_is_anga1 : forall A B C A' B' C' a , ~ CongA A B C A' B' C' -> Ang_Acute A B C a -> ~ Ang_Acute A' B' C' a.
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
    intro.
(* Goal: False *)
    unfold Ang_Acute in *.
(* Goal: b X Y Z *)
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
    spliter.
(* Goal: False *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (a A B C) (@OS Tn A B C P)) *)
    apply H.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
    apply (anga_conga a); auto.
Qed.

Lemma ex_eqaa : forall a1 a2, (exists A , exists B, exists C, Ang_Acute A B C a1 /\ Ang_Acute A B C a2)  -> EqA a1 a2.
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: @EqA Tn a1 a2 *)
    apply ex_eqa.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Ang Tn A B C a1) (@Ang Tn A B C a2)))) *)
    ex_and H A.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Ang Tn A B C a1) (@Ang Tn A B C a2)))) *)
    ex_and H0 B.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Ang Tn A B C a1) (@Ang Tn A B C a2)))) *)
    ex_and H C.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Acute Tn A B C) (forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z))))) *)
    exists A.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Acute Tn A B C) (forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z)))) *)
    exists B.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Acute Tn A B C) (forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z))) *)
    exists C.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
    split; apply is_anga_to_is_ang; auto.
Qed.

Lemma all_eqaa : forall A B C a1 a2, Ang_Acute A B C a1 -> Ang_Acute A B C a2 -> EqA a1 a2.
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: @EqA Tn a1 a2 *)
    apply ex_eqaa.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Acute Tn A B C) (forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z))))) *)
    exists A.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Acute Tn A B C) (forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z)))) *)
    exists B.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Acute Tn A B C) (forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z))) *)
    exists C.
(* Goal: @Ang Tn X Y Z a *)
    split; auto.
Qed.

Lemma is_anga_distinct : forall A B C a , Ang_Acute A B C a -> A <> B /\ C <> B.
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) C B)) *)
    apply (is_ang_distinct A B C a).
(* Goal: @Ang Tn A B C a *)
    apply is_anga_to_is_ang.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
    auto.
Qed.

Global Instance eqA_equivalence : Equivalence EqA.
Proof.
(* Goal: iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
split.
(* Goal: @Reflexive (forall (_ : @Tpoint Tn) (_ : @Tpoint Tn) (_ : @Tpoint Tn), Prop) (@EqA Tn) *)
(* Goal: @Symmetric (forall (_ : @Tpoint Tn) (_ : @Tpoint Tn) (_ : @Tpoint Tn), Prop) (@EqA Tn) *)
(* Goal: @Transitive (forall (_ : @Tpoint Tn) (_ : @Tpoint Tn) (_ : @Tpoint Tn), Prop) (@EqA Tn) *)
unfold Reflexive.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
intros.
(* Goal: @EqA Tn x x *)
(* Goal: @Symmetric (forall (_ : @Tpoint Tn) (_ : @Tpoint Tn) (_ : @Tpoint Tn), Prop) (@EqA Tn) *)
(* Goal: @Transitive (forall (_ : @Tpoint Tn) (_ : @Tpoint Tn) (_ : @Tpoint Tn), Prop) (@EqA Tn) *)
unfold EqA.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
intros;tauto.
(* Goal: @Symmetric (forall (_ : @Tpoint Tn) (_ : @Tpoint Tn) (_ : @Tpoint Tn), Prop) (@EqA Tn) *)
(* Goal: @Transitive (forall (_ : @Tpoint Tn) (_ : @Tpoint Tn) (_ : @Tpoint Tn), Prop) (@EqA Tn) *)
unfold Symmetric, EqA.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
intros.
(* Goal: iff (y A B C) (x A B C) *)
(* Goal: @Transitive (forall (_ : @Tpoint Tn) (_ : @Tpoint Tn) (_ : @Tpoint Tn), Prop) (@EqA Tn) *)
firstorder.
(* Goal: @Transitive (forall (_ : @Tpoint Tn) (_ : @Tpoint Tn) (_ : @Tpoint Tn), Prop) (@EqA Tn) *)
unfold Transitive, EqA.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
intros.
(* Goal: iff (x A B C) (z A B C) *)
rewrite H.
(* Goal: iff (a X Y Z) (b X Y Z) *)
apply H0.
Qed.

Lemma null_anga : forall A B C D a1 a2, Ang_Acute A B A a1 -> Ang_Acute C D C a2 -> EqA a1 a2.
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: @EqA Tn a1 a2 *)
    eapply (all_eqaa A B A).
(* Goal: False *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (a A B C) (@OS Tn A B C P)) *)
      apply H.
(* Goal: @Ang_Acute Tn A B A a2 *)
    eapply (is_anga_conga_is_anga C D C).
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      auto.
(* Goal: @CongA Tn C D C A B A *)
    eapply l11_21_b.
(* Goal: @Out Tn B A A *)
      apply out_trivial.
(* Goal: not (@eq (@Tpoint Tn) C D) *)
(* Goal: @Out Tn B A A *)
      apply is_anga_distinct in H0.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      tauto.
(* Goal: @Out Tn B A A *)
    apply out_trivial.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
    apply is_anga_distinct in H.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
    tauto.
Qed.

Lemma anga_distinct: forall a A B C, Q_CongA_Acute a -> a A B C -> A <> B /\ C <> B.
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) C B)) *)
    assert(Ang_Acute A B C a).
(* Goal: @Ang Tn X Y Z a *)
      split; auto.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
    apply (is_anga_distinct _ _ _ a); auto.
Qed.

Lemma out_is_len_eq : forall A B C l, Out A B C -> Len A B l -> Len A C l -> B = C.
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: @eq (@Tpoint Tn) B C *)
    assert(Cong A B A C).
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      apply (is_len_cong _ _ _ _ l); auto.
(* Goal: @eq (@Tpoint Tn) B C *)
    assert(A <> C).
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: @eq (@Tpoint Tn) B C *)
      unfold Out in H.
(* Goal: b X Y Z *)
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
      spliter.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      auto.
(* Goal: @eq (@Tpoint Tn) B C *)
    eapply (l6_11_uniqueness A A C C ); Cong.
(* Goal: @Out Tn B A A *)
    apply out_trivial.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
    auto.
Qed.

Lemma out_len_eq : forall A B C l, Q_Cong l -> Out A B C -> l A B -> l A C -> B = C.
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: @eq (@Tpoint Tn) B C *)
    apply (out_is_len_eq A _ _ l).
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      auto.
(* Goal: @Ang Tn X Y Z a *)
      split; auto.
(* Goal: @Ang Tn X Y Z a *)
    split; auto.
Qed.

Lemma ex_anga : forall A B C, Acute A B C -> exists a, Q_CongA_Acute a /\ a A B C.
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: @ex (forall (_ : @Tpoint Tn) (_ : @Tpoint Tn) (_ : @Tpoint Tn), Prop) (fun a : forall (_ : @Tpoint Tn) (_ : @Tpoint Tn) (_ : @Tpoint Tn), Prop => and (@Q_CongA_Acute Tn a) (a A B C)) *)
    exists (fun X Y Z => CongA A B C X Y Z).
(* Goal: @Q_CongA_Acute Tn b *)
    unfold Q_CongA_Acute.
(* Goal: and (@ex (@Tpoint Tn) (fun A0 : @Tpoint Tn => @ex (@Tpoint Tn) (fun B0 : @Tpoint Tn => @ex (@Tpoint Tn) (fun C0 : @Tpoint Tn => and (@Acute Tn A0 B0 C0) (forall X Y Z : @Tpoint Tn, iff (@CongA Tn A0 B0 C0 X Y Z) (@CongA Tn A B C X Y Z)))))) (@CongA Tn A B C A B C) *)
    assert (HH := acute_distincts A B C H).
(* Goal: b X Y Z *)
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
    spliter.
(* Goal: iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    split.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Acute Tn A B C) (forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z))))) *)
      exists A.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Acute Tn A B C) (forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z)))) *)
      exists B.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Acute Tn A B C) (forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z))) *)
      exists C.
(* Goal: @Ang Tn X Y Z a *)
      split; auto.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
      intros.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
      intros.
(* Goal: iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
      split.
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
        intro.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
        auto.
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
      intro.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      auto.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
    apply conga_refl; auto.
Qed.

Lemma not_null_ang_ang : forall a, Q_CongA_nNull a -> Q_CongA a.
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
    unfold Q_CongA_nNull  in H.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
    spliter; auto.
Qed.

Lemma not_null_ang_def_equiv : forall a, Q_CongA_nNull a <-> (Q_CongA a /\ exists A, exists B, exists C, a A B C /\  ~Out B A C).
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    split.
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
      intro.
(* Goal: and (@Q_CongA Tn a) (@ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (a A B C) (not (@Out Tn B A C)))))) *)
(* Goal: forall _ : and (@Q_CongA Tn a) (@ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (a A B C) (not (@Out Tn B A C)))))), @Q_CongA_nNull Tn a *)
      unfold Q_CongA_nNull in H.
(* Goal: b X Y Z *)
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
      spliter.
(* Goal: a A' B C' *)
      assert(HH:= H).
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (a A B C) (@OS Tn A B C P)) *)
      unfold Q_CongA in HH.
(* Goal: and (@Q_CongA Tn a) (@ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (a A B C) (not (@Bet Tn A B C)))))) *)
(* Goal: forall _ : and (@Q_CongA Tn a) (@ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (a A B C) (not (@Bet Tn A B C)))))), @Q_CongA_nFlat Tn a *)
      ex_and HH A.
(* Goal: and (@Q_CongA_Acute Tn a) (forall (A B C : @Tpoint Tn) (_ : a A B C), @Out Tn B A C) *)
      ex_and H1 B.
(* Goal: and (@Q_CongA Tn a) (@ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (a A B C) (not (@Bet Tn A B C)))))) *)
(* Goal: forall _ : and (@Q_CongA Tn a) (@ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (a A B C) (not (@Bet Tn A B C)))))), @Q_CongA_nFlat Tn a *)
      ex_and H2 C.
(* Goal: iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
      split.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
        auto.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Acute Tn A B C) (forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z))))) *)
      exists A.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Acute Tn A B C) (forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z)))) *)
      exists B.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Acute Tn A B C) (forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z))) *)
      exists C.
(* Goal: and (a A B C) (not (@Bet Tn A B C)) *)
(* Goal: forall _ : and (@Q_CongA Tn a) (@ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (a A B C) (not (@Bet Tn A B C)))))), @Q_CongA_nFlat Tn a *)
      assert(HH:= H3 A B C).
(* Goal: @CongA Tn A B C X Y Z *)
      destruct HH.
(* Goal: and (a A B C) (@OS Tn A B C P) *)
      assert(a A B C).
(* Goal: a C B A *)
        apply H4.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
        apply conga_refl; auto.
(* Goal: iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
      split.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
        auto.
(* Goal: not (@Bet Tn A B C) *)
(* Goal: forall _ : and (@Q_CongA Tn a) (@ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (a A B C) (not (@Bet Tn A B C)))))), @Q_CongA_nFlat Tn a *)
      apply (H0 A B C).
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      auto.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: b X Y Z *)
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
    spliter.
(* Goal: and (@Q_CongA_Acute Tn a) (forall (A B C : @Tpoint Tn) (_ : a A B C), @Out Tn B A C) *)
    ex_and H0 A.
(* Goal: and (@Q_CongA_Acute Tn a) (forall (A B C : @Tpoint Tn) (_ : a A B C), @Out Tn B A C) *)
    ex_and H1 B.
(* Goal: and (@Q_CongA_Acute Tn a) (forall (A B C : @Tpoint Tn) (_ : a A B C), @Out Tn B A C) *)
    ex_and H0 C.
(* Goal: @Q_CongA_nNull Tn a *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (a A B C) (@OS Tn A B C P)) *)
    unfold Q_CongA_nNull.
(* Goal: @Ang Tn X Y Z a *)
    split; auto.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: a A' B C' *)
    assert(CongA A0 B0 C0 A B C).
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      apply (ang_conga a); auto.
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
    intro.
(* Goal: False *)
    apply H1.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
    apply (l11_21_a A0 B0 C0); auto.
Qed.

Lemma not_flat_ang_def_equiv : forall a, Q_CongA_nFlat a <-> (Q_CongA a /\ exists A, exists B, exists C, a A B C /\  ~Bet A B C).
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    split.
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
      intro.
(* Goal: and (@Q_CongA Tn a) (@ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (a A B C) (not (@Bet Tn A B C)))))) *)
(* Goal: forall _ : and (@Q_CongA Tn a) (@ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (a A B C) (not (@Bet Tn A B C)))))), @Q_CongA_nFlat Tn a *)
      unfold Q_CongA_nFlat in H.
(* Goal: b X Y Z *)
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
      spliter.
(* Goal: a A' B C' *)
      assert(HH:= H).
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (a A B C) (@OS Tn A B C P)) *)
      unfold Q_CongA in HH.
(* Goal: and (@Q_CongA Tn a) (@ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (a A B C) (not (@Bet Tn A B C)))))) *)
(* Goal: forall _ : and (@Q_CongA Tn a) (@ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (a A B C) (not (@Bet Tn A B C)))))), @Q_CongA_nFlat Tn a *)
      ex_and HH A.
(* Goal: and (@Q_CongA_Acute Tn a) (forall (A B C : @Tpoint Tn) (_ : a A B C), @Out Tn B A C) *)
      ex_and H1 B.
(* Goal: and (@Q_CongA Tn a) (@ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (a A B C) (not (@Bet Tn A B C)))))) *)
(* Goal: forall _ : and (@Q_CongA Tn a) (@ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (a A B C) (not (@Bet Tn A B C)))))), @Q_CongA_nFlat Tn a *)
      ex_and H2 C.
(* Goal: iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
      split.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
        auto.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Acute Tn A B C) (forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z))))) *)
      exists A.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Acute Tn A B C) (forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z)))) *)
      exists B.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Acute Tn A B C) (forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z))) *)
      exists C.
(* Goal: and (a A B C) (not (@Bet Tn A B C)) *)
(* Goal: forall _ : and (@Q_CongA Tn a) (@ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (a A B C) (not (@Bet Tn A B C)))))), @Q_CongA_nFlat Tn a *)
      assert(HH:= H3 A B C).
(* Goal: @CongA Tn A B C X Y Z *)
      destruct HH.
(* Goal: and (a A B C) (@OS Tn A B C P) *)
      assert(a A B C).
(* Goal: a C B A *)
        apply H4.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
        apply conga_refl; auto.
(* Goal: iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
      split.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
        auto.
(* Goal: not (@Bet Tn A B C) *)
(* Goal: forall _ : and (@Q_CongA Tn a) (@ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (a A B C) (not (@Bet Tn A B C)))))), @Q_CongA_nFlat Tn a *)
      apply (H0 A B C).
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      auto.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: b X Y Z *)
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
    spliter.
(* Goal: and (@Q_CongA_Acute Tn a) (forall (A B C : @Tpoint Tn) (_ : a A B C), @Out Tn B A C) *)
    ex_and H0 A.
(* Goal: and (@Q_CongA_Acute Tn a) (forall (A B C : @Tpoint Tn) (_ : a A B C), @Out Tn B A C) *)
    ex_and H1 B.
(* Goal: and (@Q_CongA_Acute Tn a) (forall (A B C : @Tpoint Tn) (_ : a A B C), @Out Tn B A C) *)
    ex_and H0 C.
(* Goal: @Q_CongA_nFlat Tn a *)
    unfold Q_CongA_nFlat.
(* Goal: @Ang Tn X Y Z a *)
    split; auto.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: a A' B C' *)
    assert(CongA A0 B0 C0 A B C).
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      apply (ang_conga a); auto.
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
    intro.
(* Goal: False *)
    apply H1.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
    apply (bet_conga__bet A0 B0 C0); auto.
Qed.

Lemma ang_const : forall a A B, Q_CongA a -> A <> B -> exists C, a A B C.
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: False *)
    unfold Q_CongA in H.
(* Goal: not (@Bet Tn A B C) *)
    ex_and H A0.
(* Goal: not (@Bet Tn A B C) *)
    ex_and H1 B0.
(* Goal: not (@Bet Tn A B C) *)
    ex_and H C0.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => a A B C) *)
    apply(swap_diff) in H1.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => a A B C) *)
    assert(HH:= H2 A0 B0 C0).
(* Goal: @CongA Tn A B C X Y Z *)
    destruct HH.
(* Goal: @CongA Tn A0 B0 C0 A B A *)
    assert(a A0 B0 C0).
(* Goal: a A0 B0 C0 *)
(* Goal: @CongA Tn A0 B0 C0 A B A *)
      apply H3.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      apply conga_refl; auto.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => a A B C) *)
    assert(HH :=not_col_exists A B H0).
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => a A B C) *)
    ex_and HH P.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => a A B C) *)
    induction(eq_dec_points A0 C0).
(* Goal: False *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (a A B C) (@OS Tn A B C P)) *)
      subst C0.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Acute Tn A B C) (forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z))))) *)
      exists A.
(* Goal: a A B A *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => a A B C) *)
      assert(HH:= (H2 A B A)).
(* Goal: @CongA Tn A B C X Y Z *)
      destruct HH.
(* Goal: @CongA Tn A0 B0 C0 A B C *)
(* Goal: False *)
      apply H7.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      apply conga_trivial_1; auto.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => a A B C) *)
    assert(HH:=angle_construction_2 A0 B0 C0 A B P H H7 H1).
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
    ex_and HH C; auto.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Acute Tn A B C) (forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z))) *)
    exists C.
(* Goal: a A B C *)
    apply H2.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
    auto.
Qed.

End Angles_3.

Ltac ang_instance1 a A B C :=
	assert(tempo_ang:= ang_const a A B);
        match goal with
           |H: Q_CongA a |-  _ => assert(tempo_H:= H);apply tempo_ang in tempo_H; ex_elim tempo_H C
        end;
        clear tempo_ang.

Section Angles_4.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma ang_sym : forall a A B C, Q_CongA a -> a A B C -> a C B A.
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: False *)
    unfold Q_CongA in H.
(* Goal: not (@Bet Tn A B C) *)
    ex_and H A0.
(* Goal: not (@Bet Tn A B C) *)
    ex_and H1 B0.
(* Goal: not (@Bet Tn A B C) *)
    ex_and H C0.
(* Goal: @Out Tn B A C *)
    assert(HH:= H2 A B C).
(* Goal: @CongA Tn A B C X Y Z *)
    destruct HH.
(* Goal: a C B A *)
    apply H4 in H0.
(* Goal: a C B A *)
    apply conga_right_comm in H0.
(* Goal: a C B A *)
    assert(HH:= H2 C B A).
(* Goal: @CongA Tn A B C X Y Z *)
    destruct HH.
(* Goal: a C B A *)
    apply H5.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
    auto.
Qed.

Lemma ang_not_null_lg : forall a l A B C, Q_CongA a -> Q_Cong l -> a A B C -> l A B -> ~ Q_Cong_Null l.
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
    intro.
(* Goal: False *)
    unfold Q_CongA in H.
(* Goal: False *)
    unfold Q_Cong_Null in H3.
(* Goal: b X Y Z *)
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
    spliter.
(* Goal: False *)
    unfold Q_Cong in H0.
(* Goal: not (@Bet Tn A B C) *)
    ex_and H A0.
(* Goal: False *)
    ex_and H5 B0.
(* Goal: not (@Bet Tn A B C) *)
    ex_and H C0.
(* Goal: False *)
    assert(HH:= H6 A B C).
(* Goal: @CongA Tn A B C X Y Z *)
    destruct HH.
(* Goal: a A' B C' *)
    assert(CongA A0 B0 C0 A B C).
(* Goal: @CongA Tn A0 B0 C0 A B C *)
(* Goal: False *)
      apply H8.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      auto.
(* Goal: False *)
    apply conga_distinct in H8.
(* Goal: b X Y Z *)
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
      spliter.
(* Goal: False *)
      ex_and H0 A1.
(* Goal: False *)
(* Goal: a A B C *)
      ex_and H14 B1.
(* Goal: False *)
      assert(HH:= H0 A B).
(* Goal: @CongA Tn A B C X Y Z *)
      destruct HH.
(* Goal: False *)
      ex_and H4 A'.
(* Goal: False *)
      assert(HH:= H0 A' A').
(* Goal: @CongA Tn A B C X Y Z *)
      destruct HH.
(* Goal: False *)
      assert(Cong A1 B1 A' A').
(* Goal: @Cong Tn A1 B1 A' A' *)
(* Goal: False *)
(* Goal: a A B C *)
        apply H17.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
        auto.
(* Goal: False *)
      assert(Cong A1 B1 A B).
(* Goal: a A B C *)
(* Goal: and (a A B C) (@OS Tn A B C P) *)
        apply H15.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
        auto.
(* Goal: False *)
      apply cong_identity in H17.
(* Goal: False *)
        subst B1.
(* Goal: False *)
(* Goal: l A' A' *)
(* Goal: a A B C *)
        apply cong_symmetry in H19.
(* Goal: False *)
(* Goal: l A' A' *)
(* Goal: a A B C *)
        apply cong_identity in H19.
(* Goal: @Out Tn B A C *)
(* Goal: @Out Tn B A C *)
(* Goal: and (@Out Tn B A C) (@Q_CongA_Null_Acute Tn a) *)
        contradiction.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      auto.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
    auto.
Qed.

Lemma ang_distincts : forall a A B C, Q_CongA a -> a A B C -> A <> B /\ C <> B.
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) C B)) *)
    assert(HH:= ex_lg A B).
(* Goal: and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) C B)) *)
    ex_and HH la.
(* Goal: and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) C B)) *)
    assert(HH:= ex_lg C B).
(* Goal: and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) C B)) *)
    ex_and HH lc.
(* Goal: and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) C B)) *)
    assert(HH:= ang_not_null_lg a la A B C H H1 H0 H2).
(* Goal: and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) C B)) *)
    assert(a C B A).
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      apply ang_sym; auto.
(* Goal: and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) C B)) *)
    assert(HQ:= ang_not_null_lg a lc C B A H H3 H5 H4).
(* Goal: and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) C B)) *)
    split; intro; subst B.
(* Goal: and (not (@eq (@Tpoint Tn) A' B')) (not (@eq (@Tpoint Tn) C' B')) *)
(* Goal: @InAngle Tn C' A' B' C' *)
(* Goal: @CongA Tn A B C A' B' C' *)
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
      apply HH.
(* Goal: @Q_Cong_Null Tn lc *)
      unfold Q_Cong_Null.
(* Goal: iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
      split.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
        auto.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Acute Tn A B C) (forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z))))) *)
      exists A.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      auto.
(* Goal: False *)
    apply HQ.
(* Goal: @Q_Cong_Null Tn lc *)
    unfold Q_Cong_Null.
(* Goal: iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    split.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      auto.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Acute Tn A B C) (forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z))) *)
    exists C.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
    auto.
Qed.

Lemma anga_sym : forall a A B C, Q_CongA_Acute a -> a A B C -> a C B A.
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: @Acute Tn A B C *)
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    unfold Q_CongA_Acute in H.
(* Goal: not (@Bet Tn A B C) *)
    ex_and H A0.
(* Goal: not (@Bet Tn A B C) *)
    ex_and H1 B0.
(* Goal: not (@Bet Tn A B C) *)
    ex_and H C0.
(* Goal: @Q_CongA_Acute Tn b *)
    assert(HH:= H1 A B C).
(* Goal: @CongA Tn A B C X Y Z *)
    destruct HH.
(* Goal: a C B A *)
    apply H3 in H0.
(* Goal: a C B A *)
    apply conga_right_comm in H0.
(* Goal: a C B A *)
    assert(HH:= H1 C B A).
(* Goal: @CongA Tn A B C X Y Z *)
    destruct HH.
(* Goal: a C B A *)
    apply H4.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
    auto.
Qed.

Lemma anga_not_null_lg : forall a l A B C, Q_CongA_Acute a -> Q_Cong l -> a A B C -> l A B -> ~ Q_Cong_Null l.
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
    intro.
(* Goal: @Acute Tn A B C *)
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    unfold Q_CongA_Acute in H.
(* Goal: False *)
    unfold Q_Cong_Null in H3.
(* Goal: b X Y Z *)
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
    spliter.
(* Goal: False *)
    unfold Q_Cong in H0.
(* Goal: not (@Bet Tn A B C) *)
    ex_and H A0.
(* Goal: False *)
    ex_and H5 B0.
(* Goal: not (@Bet Tn A B C) *)
    ex_and H C0.
(* Goal: a A B C *)
(* Goal: and (a A B C) (@OS Tn A B C P) *)
    assert(HH:= H5 A B C).
(* Goal: @CongA Tn A B C X Y Z *)
    destruct HH.
(* Goal: a A' B C' *)
    assert(CongA A0 B0 C0 A B C).
(* Goal: @CongA Tn A0 B0 C0 A B C *)
(* Goal: False *)
      apply H7.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      auto.
(* Goal: False *)
    apply conga_distinct in H8.
(* Goal: b X Y Z *)
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
    spliter.
(* Goal: False *)
    ex_and H0 A1.
(* Goal: False *)
    ex_and H13 B1.
(* Goal: False *)
    assert(HH:= H0 A B).
(* Goal: @CongA Tn A B C X Y Z *)
    destruct HH.
(* Goal: False *)
    ex_and H4 A'.
(* Goal: False *)
    assert(HH:= H0 A' A').
(* Goal: @CongA Tn A B C X Y Z *)
    destruct HH.
(* Goal: False *)
    assert(Cong A1 B1 A' A').
(* Goal: @Cong Tn A1 B1 A' A' *)
(* Goal: False *)
      apply H16.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      auto.
(* Goal: False *)
    assert(Cong A1 B1 A B).
(* Goal: @Cong Tn A1 B1 A B *)
(* Goal: False *)
      apply H14.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      auto.
(* Goal: False *)
    apply cong_identity in H17.
(* Goal: False *)
    subst B1.
(* Goal: False *)
    apply cong_symmetry in H18.
(* Goal: False *)
    apply cong_identity in H18.
(* Goal: @Out Tn B A C *)
(* Goal: @Out Tn B A C *)
(* Goal: and (@Out Tn B A C) (@Q_CongA_Null_Acute Tn a) *)
    contradiction.
Qed.

Lemma anga_distincts : forall a A B C, Q_CongA_Acute a -> a A B C -> A <> B /\ C <> B.
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) C B)) *)
    assert(HH:= ex_lg A B).
(* Goal: and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) C B)) *)
    ex_and HH la.
(* Goal: and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) C B)) *)
    assert(HH:= ex_lg C B).
(* Goal: and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) C B)) *)
    ex_and HH lc.
(* Goal: and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) C B)) *)
    assert(HH:= anga_not_null_lg a la A B C H H1 H0 H2).
(* Goal: and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) C B)) *)
    assert(a C B A).
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      apply anga_sym; auto.
(* Goal: and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) C B)) *)
    assert(HQ:= anga_not_null_lg a lc C B A H H3 H5 H4).
(* Goal: and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) C B)) *)
    split; intro; subst B.
(* Goal: and (not (@eq (@Tpoint Tn) A' B')) (not (@eq (@Tpoint Tn) C' B')) *)
(* Goal: @InAngle Tn C' A' B' C' *)
(* Goal: @CongA Tn A B C A' B' C' *)
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
      apply HH.
(* Goal: @Q_Cong_Null Tn lc *)
      unfold Q_Cong_Null.
(* Goal: iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
      split.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
        auto.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Acute Tn A B C) (forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z))))) *)
      exists A.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      auto.
(* Goal: False *)
    apply HQ.
(* Goal: @Q_Cong_Null Tn lc *)
    unfold Q_Cong_Null.
(* Goal: iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    split.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      auto.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Acute Tn A B C) (forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z))) *)
    exists C.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
    auto.
Qed.

Lemma ang_const_o : forall a A B P, ~Col A B P -> Q_CongA a -> Q_CongA_nNull a -> Q_CongA_nFlat a -> exists C, a A B C /\ OS A B C P.
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: a A B A *)
    assert(HH:= H0).
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (a A B C) (@OS Tn A B C P)) *)
    unfold Q_CongA in HH.
(* Goal: a A B A *)
    ex_and HH A0.
(* Goal: a A' B C' *)
    ex_and H3 B0.
(* Goal: a A' B C' *)
    ex_and H4 C0.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (a A B C) (@OS Tn A B C P)) *)
    apply(swap_diff) in H4.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (a A B C) (@OS Tn A B C P)) *)
    assert(HH:= H5 A0 B0 C0).
(* Goal: @CongA Tn A B C X Y Z *)
    destruct HH.
(* Goal: @CongA Tn A0 B0 C0 A B A *)
    assert(a A0 B0 C0).
(* Goal: @CongA Tn A0 B0 C0 A B C *)
(* Goal: a A' B C' *)
      apply H6.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      apply conga_refl; auto.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (a A B C) (@OS Tn A B C P)) *)
    assert(HH:=ang_distincts a A0 B0 C0 H0 H8).
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (a A B C) (@OS Tn A B C P)) *)
    assert(A0 <> C0).
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
      intro.
(* Goal: False *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (a A B C) (@OS Tn A B C P)) *)
      subst C0.
(* Goal: @OS Tn A B C P *)
      unfold Q_CongA_nNull in H1.
(* Goal: b X Y Z *)
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
      spliter.
(* Goal: False *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (a A B C) (@OS Tn A B C P)) *)
      assert(HH:=H11 A0 B0 A0 H8).
(* Goal: and (not (@eq (@Tpoint Tn) A' B')) (not (@eq (@Tpoint Tn) C' B')) *)
(* Goal: @InAngle Tn C' A' B' C' *)
(* Goal: @CongA Tn A B C A' B' C' *)
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
      apply HH.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      apply out_trivial; auto.
(* Goal: b X Y Z *)
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
    spliter.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (a A B C) (@OS Tn A B C P)) *)
    assert(A <> B).
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
      intro.
(* Goal: False *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (a A B C) (@OS Tn A B C P)) *)
      subst B.
(* Goal: False *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (a A B C) (@OS Tn A B C P)) *)
      apply H.
(* Goal: @Col Tn A A P *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (a A B C) (@OS Tn A B C P)) *)
      Col.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (a A B C) (@OS Tn A B C P)) *)
    assert(HH:=angle_construction_2 A0 B0 C0 A B P H10 H9 H4).
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
    ex_and HH C; auto.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Acute Tn A B C) (forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z))) *)
    exists C.
(* Goal: and (a A B C) (@OS Tn A B C P) *)
    assert(a A B C).
(* Goal: a A B C *)
(* Goal: and (a A B C) (@OS Tn A B C P) *)
      assert(HH:= H5 A B C).
(* Goal: @CongA Tn A B C X Y Z *)
      destruct HH.
(* Goal: a A B C *)
(* Goal: and (a A B C) (@OS Tn A B C P) *)
      apply H15.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      auto.
(* Goal: iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    split.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      auto.
(* Goal: @OS Tn A B C P *)
    induction H14.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      auto.
(* Goal: @OS Tn A B C P *)
    unfold Q_CongA_nNull in H1.
(* Goal: b X Y Z *)
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
    spliter.
(* Goal: @OS Tn A B C P *)
    assert(HH:= H16 A B C H15).
(* Goal: @OS Tn A B C P *)
    unfold Q_CongA_nFlat in H2.
(* Goal: b X Y Z *)
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
    spliter.
(* Goal: @OS Tn A B C P *)
    assert(Hh:=H17 A B C H15).
(* Goal: @OS Tn A B C P *)
    apply False_ind.
(* Goal: False *)
    assert(HH0:=ang_distincts a A B C H0 H15).
(* Goal: b X Y Z *)
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
    spliter.
(* Goal: False *)
    assert(HP:=or_bet_out A B C).
(* Goal: False *)
    induction HP.
(* Goal: @Out Tn B A C *)
(* Goal: @Out Tn B A C *)
(* Goal: and (@Out Tn B A C) (@Q_CongA_Null_Acute Tn a) *)
      contradiction.
(* Goal: False *)
    induction H20.
(* Goal: @Out Tn B A C *)
(* Goal: @Out Tn B A C *)
(* Goal: and (@Out Tn B A C) (@Q_CongA_Null_Acute Tn a) *)
      contradiction.
(* Goal: @Out Tn B A C *)
(* Goal: @Out Tn B A C *)
(* Goal: and (@Out Tn B A C) (@Q_CongA_Null_Acute Tn a) *)
    contradiction.
Qed.

Lemma anga_const : forall a A B, Q_CongA_Acute a -> A <> B -> exists C, a A B C.
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: @Q_CongA Tn a *)
(* Goal: forall (A B C : @Tpoint Tn) (_ : a A B C), not (@Bet Tn A B C) *)
    apply anga_is_ang in H.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
    apply ang_const; auto.
Qed.

End Angles_4.

Ltac anga_instance1 a A B C :=
	assert(tempo_anga:= anga_const a A B);
        match goal with
           |H: Q_CongA_Acute a |-  _ => assert(tempo_H:= H); apply tempo_anga in tempo_H; ex_elim tempo_H C
        end;
        clear tempo_anga.

Section Angles_5.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma null_anga_null_anga' : forall a, Q_CongA_Null_Acute a <-> is_null_anga' a.
Proof.
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
    intro.
(* Goal: iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    split.
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
      intro.
(* Goal: @is_null_anga' Tn a *)
(* Goal: forall _ : @is_null_anga' Tn a, @Q_CongA_Null_Acute Tn a *)
      unfold Q_CongA_Null_Acute in H.
(* Goal: @is_null_anga' Tn a *)
(* Goal: forall _ : @is_null_anga' Tn a, @Q_CongA_Null_Acute Tn a *)
      unfold is_null_anga'.
(* Goal: b X Y Z *)
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
      spliter.
(* Goal: iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
      split.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
        auto.
(* Goal: @Q_CongA_Acute Tn b *)
      anga_instance a A B C.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (a A B C) (@Out Tn B A C)))) *)
(* Goal: forall _ : @is_null_anga' Tn a, @Q_CongA_Null_Acute Tn a *)
      assert(HH:= H0 A B C H1).
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Acute Tn A B C) (forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z))))) *)
      exists A.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Acute Tn A B C) (forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z)))) *)
      exists B.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Acute Tn A B C) (forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z))) *)
      exists C.
(* Goal: @Ang Tn X Y Z a *)
      split; auto.
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
    intro.
(* Goal: @Q_CongA_Null_Acute Tn a *)
    unfold is_null_anga' in H.
(* Goal: @Q_CongA_Null_Acute Tn a *)
    unfold Q_CongA_Null_Acute.
(* Goal: b X Y Z *)
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
    spliter.
(* Goal: and (@Q_CongA_Acute Tn a) (forall (A B C : @Tpoint Tn) (_ : a A B C), @Out Tn B A C) *)
    ex_and H0 A.
(* Goal: and (@Q_CongA_Acute Tn a) (forall (A B C : @Tpoint Tn) (_ : a A B C), @Out Tn B A C) *)
    ex_and H1 B.
(* Goal: and (@Q_CongA_Acute Tn a) (forall (A B C : @Tpoint Tn) (_ : a A B C), @Out Tn B A C) *)
    ex_and H0 C.
(* Goal: @Ang Tn X Y Z a *)
    split; auto.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: @Out Tn B0 A0 C0 *)
    assert(CongA A B C A0 B0 C0).
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      apply (anga_conga a); auto.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
    apply (l11_21_a A B C); auto.
Qed.

Lemma is_null_anga_out : forall a A B C, Q_CongA_Acute a -> a A B C -> Q_CongA_Null_Acute a -> Out B A C.
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: @Out Tn B A C *)
    unfold Q_CongA_Null_Acute in H1.
(* Goal: b X Y Z *)
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
    spliter.
(* Goal: @Out Tn B A C *)
    assert(HH:= (H2 A B C)).
(* Goal: and (not (@eq (@Tpoint Tn) A' B')) (not (@eq (@Tpoint Tn) C' B')) *)
(* Goal: @InAngle Tn C' A' B' C' *)
(* Goal: @CongA Tn A B C A' B' C' *)
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    apply HH.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
    auto.
Qed.


Lemma acute_not_bet : forall A B C, Acute A B C -> ~Bet A B C.
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: not (@Bet Tn A B C) *)
    unfold Acute in H.
(* Goal: not (@Bet Tn A B C) *)
    ex_and H A0.
(* Goal: not (@Bet Tn A B C) *)
    ex_and H0 B0.
(* Goal: not (@Bet Tn A B C) *)
    ex_and H C0.
(* Goal: not (@Bet Tn A B C) *)
    unfold LtA in H0.
(* Goal: b X Y Z *)
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
    spliter.
(* Goal: not (@Bet Tn A B C) *)
    unfold LeA in H0.
(* Goal: not (@Bet Tn A B C) *)
    ex_and H0 P.
(* Goal: not (@Bet Tn A B C) *)
    unfold InAngle in H0.
(* Goal: b X Y Z *)
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
    spliter.
(* Goal: not (@Bet Tn A B C) *)
    ex_and H5 X.
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
    intro.
(* Goal: False *)
    apply conga_distinct in H2.
(* Goal: b X Y Z *)
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
    spliter.
(* Goal: False *)
    assert(A<>C) by (intro; Between).
(* Goal: False *)
    induction H6.
(* Goal: False *)
(* Goal: False *)
      subst X.
(* Goal: False *)
      apply H1.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      apply conga_line; auto.
(* Goal: False *)
    assert(Bet A0 B0 P).
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      apply (bet_conga__bet A B C); auto.
(* Goal: False *)
    assert(Bet A0 B0 C0).
(* Goal: @Bet Tn A0 B0 C0 *)
(* Goal: False *)
      unfold Out in H6.
(* Goal: b X Y Z *)
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
      spliter.
(* Goal: @Bet Tn A0 B0 C0 *)
(* Goal: False *)
      induction H15.
(* Goal: @Bet Tn A0 B0 C0 *)
(* Goal: False *)
        eBetween.
(* Goal: @Bet Tn A0 B0 C0 *)
(* Goal: False *)
      eBetween.
(* Goal: False *)
    apply H1.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
    apply (conga_line A B C); auto.
Qed.

Lemma anga_acute : forall a A B C , Q_CongA_Acute a -> a A B C -> Acute A B C.
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: @Acute Tn A B C *)
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    unfold Q_CongA_Acute in H.
(* Goal: not (@Bet Tn A B C) *)
    ex_and H A0.
(* Goal: not (@Bet Tn A B C) *)
    ex_and H1 B0.
(* Goal: not (@Bet Tn A B C) *)
    ex_and H C0.
(* Goal: @Acute Tn A B C *)
    assert(HH:= acute_lea_acute A B C A0 B0 C0).
(* Goal: and (not (@eq (@Tpoint Tn) A' B')) (not (@eq (@Tpoint Tn) C' B')) *)
(* Goal: @InAngle Tn C' A' B' C' *)
(* Goal: @CongA Tn A B C A' B' C' *)
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    apply HH.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      auto.
(* Goal: @LeA Tn A B C A' B' C' *)
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    unfold LeA.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn A0 X C0) (or (@eq (@Tpoint Tn) X B0) (@Out Tn B0 X C0))) *)
(* Goal: @CongA Tn A B C A0 B0 C0 *)
    exists C0.
(* Goal: iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    split.
(* Goal: @InAngle Tn C0 A0 B0 C0 *)
(* Goal: @CongA Tn A B C A0 B0 C0 *)
      unfold InAngle.
(* Goal: and (not (@eq (@Tpoint Tn) A0 B0)) (and (not (@eq (@Tpoint Tn) C0 B0)) (and (not (@eq (@Tpoint Tn) C0 B0)) (@ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn A0 X C0) (or (@eq (@Tpoint Tn) X B0) (@Out Tn B0 X C0)))))) *)
(* Goal: @CongA Tn A B C A0 B0 C0 *)
      apply acute_distincts in H.
(* Goal: b X Y Z *)
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
      spliter.
(* Goal: @Ang Tn X Y Z a *)
      repeat split; auto.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn A0 X C0) (or (@eq (@Tpoint Tn) X B0) (@Out Tn B0 X C0))) *)
(* Goal: @CongA Tn A B C A0 B0 C0 *)
      exists C0.
(* Goal: iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
      split.
(* Goal: @Bet Tn B A C *)
(* Goal: and (@Out Tn B A C) (@Q_CongA_Null_Acute Tn a) *)
        Between.
(* Goal: or (@Bet Tn B A C) (@Bet Tn B C A) *)
(* Goal: or (@Bet Tn B A C) (@Bet Tn B C A) *)
(* Goal: a A B C *)
      right.
(* Goal: @Out Tn B A A *)
      apply out_trivial.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      auto.
(* Goal: not (@Bet Tn A B C) *)
    assert(HP:= H1 A B C).
(* Goal: a A' B' C' *)
(* Goal: @Acute Tn A B C *)
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    destruct HP.
(* Goal: @CongA Tn A B C A0 B0 C0 *)
    apply conga_sym.
(* Goal: a A0 B0 C0 *)
(* Goal: @CongA Tn A0 B0 C0 A B A *)
    apply H3.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
    auto.
Qed.

Lemma not_null_not_col : forall a A B C, Q_CongA_Acute a -> ~ Q_CongA_Null_Acute a -> a A B C -> ~Col A B C.
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
    intro.
(* Goal: iff (a X Y Z) (b X Y Z) *)
    apply H0.
(* Goal: @Q_CongA_Null_Acute Tn a *)
    unfold Q_CongA_Null_Acute.
(* Goal: iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    split.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      auto.
(* Goal: @Out Tn B A C *)
    assert(Acute A B C).
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      apply (anga_acute a); auto.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: and (@Out Tn B A C) (@Q_CongA_Null_Acute Tn a) *)
    assert(Out B A C).
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      apply acute_col__out; auto.
(* Goal: @Out Tn B0 A0 C0 *)
    assert(HH:= anga_conga a A B C A0 B0 C0 H H1 H4).
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
    apply (l11_21_a A B C); auto.
Qed.


Lemma ang_cong_ang : forall a A B C A' B' C', Q_CongA a -> a A B C -> CongA A B C A' B' C' -> a A' B' C'.
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: a A' B' C' *)
    assert(Ang A B C a).
(* Goal: @Ang Tn A B C a *)
(* Goal: a A' B' C' *)
      unfold Ang.
(* Goal: @Ang Tn X Y Z a *)
      split; auto.
(* Goal: a A' B' C' *)
(* Goal: @Acute Tn A B C *)
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    assert(Ang A' B' C' a).
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      apply (is_ang_conga_is_ang A B C); auto.
(* Goal: a A' B' C' *)
    unfold Ang in H3.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
    tauto.
Qed.

Lemma is_null_ang_out : forall a A B C, Q_CongA a -> a A B C -> Q_CongA_Null a -> Out B A C.
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: @Out Tn B A C *)
    unfold Q_CongA_Null in H1.
(* Goal: b X Y Z *)
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
    spliter.
(* Goal: @Out Tn B A C *)
    assert(HH:= (H2 A B C)).
(* Goal: and (not (@eq (@Tpoint Tn) A' B')) (not (@eq (@Tpoint Tn) C' B')) *)
(* Goal: @InAngle Tn C' A' B' C' *)
(* Goal: @CongA Tn A B C A' B' C' *)
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    apply HH.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
    auto.
Qed.

Lemma out_null_ang : forall a A B C, Q_CongA a -> a A B C -> Out B A C -> Q_CongA_Null a.
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: @Q_CongA_Null Tn a *)
    unfold Q_CongA_Null.
(* Goal: iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    split.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      auto.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: @Out Tn B0 A0 C0 *)
    assert(HH:=l11_21_a A B C A0 B0 C0 H1).
(* Goal: and (not (@eq (@Tpoint Tn) A' B')) (not (@eq (@Tpoint Tn) C' B')) *)
(* Goal: @InAngle Tn C' A' B' C' *)
(* Goal: @CongA Tn A B C A' B' C' *)
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    apply HH.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
    apply (ang_conga a); auto.
Qed.

Lemma bet_flat_ang : forall a A B C, Q_CongA a -> a A B C -> Bet A B C -> Ang_Flat a.
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: @Ang_Flat Tn a *)
    unfold Ang_Flat.
(* Goal: iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    split.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      auto.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: @Bet Tn A0 B0 C0 *)
    assert(HH:=bet_conga__bet A B C A0 B0 C0 H1).
(* Goal: and (not (@eq (@Tpoint Tn) A' B')) (not (@eq (@Tpoint Tn) C' B')) *)
(* Goal: @InAngle Tn C' A' B' C' *)
(* Goal: @CongA Tn A B C A' B' C' *)
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    apply HH.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
    apply (ang_conga a); auto.
Qed.

Lemma out_null_anga : forall a A B C, Q_CongA_Acute a -> a A B C -> Out B A C -> Q_CongA_Null_Acute a.
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: @Q_CongA_Null_Acute Tn a *)
    unfold Q_CongA_Null_Acute.
(* Goal: iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    split.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      auto.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: @Out Tn B0 A0 C0 *)
    assert(HH:=l11_21_a A B C A0 B0 C0 H1).
(* Goal: and (not (@eq (@Tpoint Tn) A' B')) (not (@eq (@Tpoint Tn) C' B')) *)
(* Goal: @InAngle Tn C' A' B' C' *)
(* Goal: @CongA Tn A B C A' B' C' *)
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    apply HH.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
    apply (anga_conga a); auto.
Qed.

Lemma anga_not_flat : forall a, Q_CongA_Acute a -> Q_CongA_nFlat a.
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: @Q_CongA_nFlat Tn a *)
    unfold Q_CongA_nFlat.
(* Goal: iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    split.
(* Goal: @Q_CongA Tn a *)
(* Goal: forall (A B C : @Tpoint Tn) (_ : a A B C), not (@Bet Tn A B C) *)
      apply anga_is_ang in H.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      auto.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: not (@Bet Tn A B C) *)
    assert(HH:= anga_acute a A B C H H0).
(* Goal: @Acute Tn A B C *)
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    unfold Q_CongA_Acute in H.
(* Goal: not (@Bet Tn A B C) *)
    ex_and H A0.
(* Goal: not (@Bet Tn A B C) *)
    ex_and H1 B0.
(* Goal: not (@Bet Tn A B C) *)
    ex_and H C0.
(* Goal: not (@Bet Tn A B C) *)
    assert(HP:= H1 A B C).
(* Goal: not (@Bet Tn A B C) *)
    apply acute_not_bet.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
    auto.
Qed.


Lemma anga_const_o : forall a A B P, ~Col A B P -> ~ Q_CongA_Null_Acute a -> Q_CongA_Acute a -> exists C, a A B C /\ OS A B C P.
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: @Q_CongA_Acute Tn b *)
    assert(Q_CongA a).
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      apply anga_is_ang; auto.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (a A B C) (@OS Tn A B C P)) *)
    assert(Q_CongA_nNull a).
(* Goal: @Q_CongA_nNull Tn a *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (a A B C) (@OS Tn A B C P)) *)
      unfold Q_CongA_nNull.
(* Goal: iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
      split.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
        auto.
(* Goal: forall (A B C : @Tpoint Tn) (_ : a A B C), not (@Out Tn B A C) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (a A B C) (@OS Tn A B C P)) *)
      intros A' B' C' HP.
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
      intro.
(* Goal: iff (a X Y Z) (b X Y Z) *)
      apply H0.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      eapply (out_null_anga a A' B' C'); auto.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (a A B C) (@OS Tn A B C P)) *)
    assert(Q_CongA_nFlat a).
(* Goal: @Q_CongA_nFlat Tn a *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (a A B C) (@OS Tn A B C P)) *)
      apply anga_not_flat.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      auto.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (a A B C) (@OS Tn A B C P)) *)
    assert(HH:= ang_const_o a A B P H H2 H3 H4).
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
    auto.
Qed.

Lemma anga_conga_anga : forall a A B C A' B' C' , Q_CongA_Acute a -> a A B C -> CongA A B C A' B' C' -> a A' B' C'.
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: @Acute Tn A B C *)
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    unfold Q_CongA_Acute in H.
(* Goal: not (@Bet Tn A B C) *)
    ex_and H A0.
(* Goal: a A B A *)
    ex_and H2 B0.
(* Goal: not (@Bet Tn A B C) *)
    ex_and H C0.
(* Goal: @Out Tn B A C *)
    assert(HH := H2 A B C).
    assert(HP := H2 A' B' C').
(* Goal: @CongA Tn A B C X Y Z *)
    destruct HH.
(* Goal: a A' B' C' *)
(* Goal: @Acute Tn A B C *)
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    destruct HP.
(* Goal: a C B A *)
    apply H4 in H0.
    assert(CongA A0 B0 C0 A' B' C').
      eapply conga_trans.
(* Goal: iff (a X Y Z) (b X Y Z) *)
        apply H0.
(* Goal: False *)
      apply H1.
(* Goal: a C B A *)
    apply H5.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
    auto.
Qed.

Lemma anga_out_anga : forall a A B C A' C', Q_CongA_Acute a -> a A B C -> Out B A A' -> Out B C C' -> a A' B C'.
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: a A' B C' *)
    assert(HH:= H).
(* Goal: a A B A *)
    unfold Q_CongA_Acute in HH.
(* Goal: a A B A *)
    ex_and HH A0.
(* Goal: a A' B C' *)
    ex_and H3 B0.
(* Goal: a A' B C' *)
    ex_and H4 C0.
(* Goal: a A' B C' *)
    assert(HP:= H4 A B C).
(* Goal: a A' B' C' *)
(* Goal: @Acute Tn A B C *)
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    destruct HP.
(* Goal: a A' B C' *)
    assert(CongA A0 B0 C0 A B C).
(* Goal: @CongA Tn A0 B0 C0 A B C *)
(* Goal: a A' B C' *)
      apply H6.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      auto.
(* Goal: a A' B C' *)
    assert(HP:= anga_distincts a A B C H H0).
(* Goal: b X Y Z *)
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
    spliter.
(* Goal: a A' B C' *)
    assert(CongA A B C A' B C').
(* Goal: @CongA Tn A B C A' B C' *)
(* Goal: a A' B C' *)
      apply (out_conga A B C A B C).
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
        apply conga_refl; auto.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
        apply out_trivial; auto.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
        apply out_trivial; auto.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
        auto.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      auto.
(* Goal: a A' B C' *)
    assert(HH:= H4 A' B C').
(* Goal: @CongA Tn A B C X Y Z *)
    destruct HH.
(* Goal: a A' B C' *)
    apply H11.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
    apply (conga_trans _ _ _ A B C); auto.
Qed.

Lemma out_out_anga : forall a A B C A' B' C', Q_CongA_Acute a -> Out B A C -> Out B' A' C' -> a A B C -> a A' B' C'.
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: a A' B' C' *)
    assert(CongA A B C A' B' C').
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      apply l11_21_b; auto.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
    apply (anga_conga_anga a A B C); auto.
Qed.

Lemma is_null_all : forall a A B, A <> B -> Q_CongA_Null_Acute a -> a A B A.
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: a A B A *)
    unfold Q_CongA_Null_Acute in H0.
(* Goal: b X Y Z *)
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
    spliter.
(* Goal: a A B A *)
    assert(HH:= H0).
(* Goal: a A B A *)
    unfold Q_CongA_Acute in HH.
(* Goal: a A B A *)
    ex_and HH A0.
(* Goal: a A B A *)
    ex_and H2 B0.
(* Goal: a A B A *)
    ex_and H3 C0.
(* Goal: a A B A *)
    apply acute_distincts in H2.
(* Goal: b X Y Z *)
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
    spliter.
(* Goal: a A0 B0 C0 *)
(* Goal: @CongA Tn A0 B0 C0 A B A *)
    apply H3.
(* Goal: @CongA Tn A0 B0 C0 A B A *)
    assert (a A0 B0 C0).
(* Goal: a A0 B0 C0 *)
(* Goal: @CongA Tn A0 B0 C0 A B A *)
      apply H3.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      apply conga_refl; auto.
(* Goal: @CongA Tn A0 B0 C0 A B A *)
    assert(HH:= (H1 A0 B0 C0 H5)).
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
    apply l11_21_b; auto.
(* Goal: @Out Tn B A A *)
    apply out_trivial.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
    auto.
Qed.

Lemma anga_col_out : forall a A B C, Q_CongA_Acute a -> a A B C -> Col A B C -> Out B A C.
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: @Out Tn B A C *)
    assert(Acute A B C).
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      apply (anga_acute a); auto.
(* Goal: @Out Tn B A C *)
    unfold Col in H1.
(* Goal: @Out Tn B A C *)
(* Goal: and (@Out Tn B A C) (@Q_CongA_Null_Acute Tn a) *)
    induction H1.
(* Goal: @Out Tn B A C *)
(* Goal: @Out Tn B A C *)
      apply acute_not_bet in H2.
(* Goal: @Out Tn B A C *)
(* Goal: @Out Tn B A C *)
(* Goal: and (@Out Tn B A C) (@Q_CongA_Null_Acute Tn a) *)
      contradiction.
(* Goal: @Out Tn B A C *)
(* Goal: and (@Out Tn B A C) (@Q_CongA_Null_Acute Tn a) *)
    unfold Out.
(* Goal: and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) C B)) (or (@Bet Tn B A C) (@Bet Tn B C A))) *)
    apply (anga_distinct a A B C) in H.
(* Goal: b X Y Z *)
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
      spliter.
(* Goal: @Ang Tn X Y Z a *)
      repeat split; auto.
(* Goal: @Out Tn B A C *)
(* Goal: and (@Out Tn B A C) (@Q_CongA_Null_Acute Tn a) *)
      induction H1.
(* Goal: or (@Bet Tn B A C) (@Bet Tn B C A) *)
(* Goal: or (@Bet Tn B A C) (@Bet Tn B C A) *)
(* Goal: a A B C *)
        right.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
        auto.
(* Goal: or (@Bet Tn B A C) (@Bet Tn B C A) *)
(* Goal: and (@Out Tn B A C) (@Q_CongA_Null_Acute Tn a) *)
      left.
(* Goal: @Bet Tn B A C *)
(* Goal: and (@Out Tn B A C) (@Q_CongA_Null_Acute Tn a) *)
      Between.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
    auto.
Qed.

Lemma ang_not_lg_null : forall a la lc A B C, Q_Cong la -> Q_Cong lc -> Q_CongA a ->
 la A B -> lc C B -> a A B C -> ~ Q_Cong_Null la /\ ~ Q_Cong_Null lc.
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: and (not (@Q_Cong_Null Tn la)) (not (@Q_Cong_Null Tn lc)) *)
    assert(HH:=ang_distincts a A B C H1 H4).
(* Goal: b X Y Z *)
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
    spliter.
(* Goal: iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    split.
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
      intro.
(* Goal: False *)
      unfold Q_Cong_Null in H7.
(* Goal: b X Y Z *)
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
      spliter.
(* Goal: False *)
      ex_and H8 P.
(* Goal: False *)
(* Goal: not (@Q_Cong_Null Tn lc) *)
      assert(HH:= lg_cong la A B P P H H2 H9).
(* Goal: False *)
      apply cong_identity in HH.
(* Goal: @Out Tn B A C *)
(* Goal: @Out Tn B A C *)
(* Goal: and (@Out Tn B A C) (@Q_CongA_Null_Acute Tn a) *)
      contradiction.
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
    intro.
(* Goal: False *)
    unfold Q_Cong_Null in H7.
(* Goal: b X Y Z *)
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
    spliter.
(* Goal: False *)
    ex_and H8 P.
(* Goal: False *)
    assert(HH:= lg_cong lc C B P P H0 H3 H9).
(* Goal: False *)
    apply cong_identity in HH.
(* Goal: @Out Tn B A C *)
(* Goal: @Out Tn B A C *)
(* Goal: and (@Out Tn B A C) (@Q_CongA_Null_Acute Tn a) *)
    contradiction.
Qed.

Lemma anga_not_lg_null : forall a la lc A B C, Q_Cong la -> Q_Cong lc ->
 Q_CongA_Acute a -> la A B -> lc C B -> a A B C -> ~ Q_Cong_Null la /\ ~ Q_Cong_Null lc.
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: and (not (@Q_Cong_Null Tn la)) (not (@Q_Cong_Null Tn lc)) *)
    apply anga_is_ang in H1.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
    apply(ang_not_lg_null a la lc A B C); auto.
Qed.

Lemma anga_col_null : forall a A B C, Q_CongA_Acute a -> a A B C -> Col A B C -> Out B A C /\ Q_CongA_Null_Acute a.
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: and (@Out Tn B A C) (@Q_CongA_Null_Acute Tn a) *)
    assert(HH:= anga_distincts a A B C H H0).
(* Goal: b X Y Z *)
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
    spliter.
(* Goal: and (@Out Tn B A C) (@Q_CongA_Null_Acute Tn a) *)
    assert(Out B A C).
(* Goal: @Out Tn B A C *)
(* Goal: and (@Out Tn B A C) (@Q_CongA_Null_Acute Tn a) *)
      induction H1.
(* Goal: @Out Tn B A C *)
(* Goal: @Out Tn B A C *)
(* Goal: and (@Out Tn B A C) (@Q_CongA_Null_Acute Tn a) *)
        assert(HP:=anga_acute a A B C H H0).
(* Goal: @Out Tn B A C *)
(* Goal: @Out Tn B A C *)
(* Goal: and (@Out Tn B A C) (@Q_CongA_Null_Acute Tn a) *)
        assert(HH:=acute_not_bet A B C HP).
(* Goal: @Out Tn B A C *)
(* Goal: @Out Tn B A C *)
(* Goal: and (@Out Tn B A C) (@Q_CongA_Null_Acute Tn a) *)
        contradiction.
(* Goal: @Out Tn B A C *)
(* Goal: and (@Out Tn B A C) (@Q_CongA_Null_Acute Tn a) *)
      induction H1.
(* Goal: @Out Tn B A C *)
(* Goal: and (@Out Tn B A C) (@Q_CongA_Null_Acute Tn a) *)
        unfold Out.
(* Goal: @Ang Tn X Y Z a *)
        repeat split; auto.
(* Goal: @Out Tn B A C *)
(* Goal: and (@Out Tn B A C) (@Q_CongA_Null_Acute Tn a) *)
      unfold Out.
(* Goal: @Ang Tn X Y Z a *)
      repeat split; auto.
(* Goal: or (@Bet Tn B A C) (@Bet Tn B C A) *)
(* Goal: and (@Out Tn B A C) (@Q_CongA_Null_Acute Tn a) *)
      left.
(* Goal: @Bet Tn B A C *)
(* Goal: and (@Out Tn B A C) (@Q_CongA_Null_Acute Tn a) *)
      Between.
(* Goal: iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    split.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      auto.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
    apply (out_null_anga a A B C); auto.
Qed.

Lemma eqA_preserves_ang: forall a b, Q_CongA a -> EqA a b -> Q_CongA b.
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
intros.
(* Goal: @Q_CongA Tn b *)
unfold Q_CongA in *.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) C B)) (forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z)))))) *)
decompose [ex and] H.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) C B)) (forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z)))))) *)
exists x. exists x0. exists x1.
(* Goal: iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
split.
(* Goal: not (@eq (@Tpoint Tn) x1 x0) *)
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn x x0 x1 X Y Z) (b X Y Z) *)
assumption.
(* Goal: iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
split.
(* Goal: not (@eq (@Tpoint Tn) x1 x0) *)
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn x x0 x1 X Y Z) (b X Y Z) *)
assumption.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
intros.
(* Goal: iff (@CongA Tn x x0 x1 X Y Z) (b X Y Z) *)
rewrite H4.
(* Goal: iff (a X Y Z) (b X Y Z) *)
unfold EqA in H0.
(* Goal: iff (a X Y Z) (b X Y Z) *)
apply H0.
Qed.

Lemma eqA_preserves_anga : forall a b, Q_CongA_Acute a -> Q_CongA b -> EqA a b -> Q_CongA_Acute b.
Proof.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: @Q_CongA_Acute Tn b *)
    assert (Q_CongA a).
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
        apply eqA_preserves_ang with b;auto.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
        symmetry;auto.
(* Goal: @Q_CongA_Acute Tn b *)
    unfold EqA in H1.
(* Goal: @Q_CongA_Acute Tn b *)
    anga_instance a A B C.

(* Goal: @Q_CongA_Acute Tn b *)
    assert(HH:= H1 A B C).
(* Goal: @CongA Tn A B C X Y Z *)
    destruct HH.
(* Goal: @Q_CongA_Acute Tn b *)
    unfold Q_CongA_Acute.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Acute Tn A B C) (forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z))))) *)
    exists A.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Acute Tn A B C) (forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z)))) *)
    exists B.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Acute Tn A B C) (forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z))) *)
    exists C.
(* Goal: iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    split.
(* Goal: @Acute Tn A B C *)
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
      unfold Q_CongA_Acute in H.
(* Goal: @Acute Tn A B C *)
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
      ex_and H A'.
(* Goal: @Acute Tn A B C *)
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
      ex_and H6 B'.
(* Goal: @Acute Tn A B C *)
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
      ex_and H C'.
(* Goal: @Acute Tn A B C *)
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
      assert(a A' B' C').
(* Goal: a A' B' C' *)
(* Goal: @Acute Tn A B C *)
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
        assert(HP:= H6 A B C).
(* Goal: a A' B' C' *)
(* Goal: @Acute Tn A B C *)
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
        destruct HP.
(* Goal: a A' B' C' *)
(* Goal: @Acute Tn A B C *)
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
        assert(CongA A B C A' B' C') by (apply conga_sym;auto).
(* Goal: a A' B' C' *)
(* Goal: @Acute Tn A B C *)
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
        assert(HP:=is_ang_conga_is_ang A B C A' B' C' a).
(* Goal: a A' B' C' *)
(* Goal: @Acute Tn A B C *)
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
        assert(Ang A' B' C' a).
(* Goal: @Ang Tn A' B' C' a *)
(* Goal: a A' B' C' *)
(* Goal: @Acute Tn A B C *)
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
          apply HP.
(* Goal: @Ang Tn X Y Z a *)
            split; auto.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
          auto.
(* Goal: a A' B' C' *)
(* Goal: @Acute Tn A B C *)
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
        unfold Ang in H10.
(* Goal: b X Y Z *)
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
        spliter.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
        auto.
(* Goal: @Acute Tn A B C *)
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
      apply (acute_lea_acute _ _ _ A' B' C').
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
        auto.
(* Goal: @LeA Tn A B C A' B' C' *)
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
      unfold LeA.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@InAngle Tn P A' B' C') (@CongA Tn A B C A' B' P)) *)
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
      exists C'.
(* Goal: iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
      split.
(* Goal: @InAngle Tn C' A' B' C' *)
(* Goal: @CongA Tn A B C A' B' C' *)
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
        assert (HH:= is_ang_distinct A' B' C' a).
(* Goal: @InAngle Tn C' A' B' C' *)
(* Goal: @CongA Tn A B C A' B' C' *)
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
        assert( A' <> B' /\ C' <> B').
(* Goal: and (not (@eq (@Tpoint Tn) A' B')) (not (@eq (@Tpoint Tn) C' B')) *)
(* Goal: @InAngle Tn C' A' B' C' *)
(* Goal: @CongA Tn A B C A' B' C' *)
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
          apply HH.
(* Goal: @Ang Tn X Y Z a *)
          split; auto.
(* Goal: b X Y Z *)
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
        spliter.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
        apply inangle3123; auto.
(* Goal: @CongA Tn A B C X Y Z *)
      eapply (is_ang_conga _ _ _ _ _ _ a).
(* Goal: @Ang Tn X Y Z a *)
        split; auto.
(* Goal: @Ang Tn X Y Z a *)
      split; auto.
(* Goal: forall X Y Z : @Tpoint Tn, iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    intros.
(* Goal: iff (@CongA Tn A B C X Y Z) (b X Y Z) *)
    split.
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
      intro.
(* Goal: @CongA Tn A B C X Y Z *)
      assert(HH:= H1 X Y Z).
(* Goal: @CongA Tn A B C X Y Z *)
      destruct HH.
(* Goal: b X Y Z *)
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
      assert(Ang X Y Z a).
(* Goal: @Ang Tn X Y Z a *)
(* Goal: b X Y Z *)
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
        eapply (is_ang_conga_is_ang A B C).
(* Goal: @Ang Tn X Y Z a *)
          split; auto.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
        auto.
(* Goal: b X Y Z *)
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
      unfold Ang in H9.
(* Goal: b X Y Z *)
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
      spliter.
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      auto.
(* Goal: forall _ : b X Y Z, @CongA Tn A B C X Y Z *)
    intro.
(* Goal: @CongA Tn A B C X Y Z *)
    assert(HH:= H1 X Y Z).
(* Goal: @CongA Tn A B C X Y Z *)
    destruct HH.
(* Goal: @CongA Tn A B C X Y Z *)
    assert(a X Y Z).
(* Goal: a X Y Z *)
(* Goal: @CongA Tn A B C X Y Z *)
      auto.
(* Goal: @CongA Tn A B C X Y Z *)
    eapply (is_ang_conga _ _ _ _ _ _ a).
(* Goal: @Ang Tn X Y Z a *)
      split; auto.
(* Goal: @Ang Tn X Y Z a *)
    split; auto.
Qed.

End Angles_5.