Require Export GeoCoq.Tarski_dev.Annexes.suma.

Section HalfAngle.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.


Definition HalfA P A O B := ~ Bet A O B /\ InAngle P A O B /\ CongA A O P B O P.

Lemma halfa_distincts : forall P A O B, HalfA P A O B -> O <> A /\ O <> B /\ O <> P.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : HalfA A B C D), @Coplanar Tn A B C D *)
  unfold HalfA.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : and (not (@Bet Tn B C D)) (and (@InAngle Tn A B C D) (@CongA Tn B C A D C A))), @Coplanar Tn A B C D *)
  intros.
(* Goal: @SumA Tn A' O' B' A' O' B' A O B *)
  spliter.
(* Goal: @SumA Tn D E F D E F D' E' F' *)
  assert_diffs.
(* Goal: and (not (@eq (@Tpoint Tn) O' A')) (and (not (@eq (@Tpoint Tn) O' B')) (and (not (@eq (@Tpoint Tn) O A)) (not (@eq (@Tpoint Tn) O B)))) *)
  repeat split; auto.
Qed.

Lemma halfa__suma : forall P A O B, HalfA P A O B -> SumA A O P A O P A O B.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : HalfA A B C D), @Coplanar Tn A B C D *)
  unfold HalfA.
(* Goal: forall (P A O B : @Tpoint Tn) (_ : and (not (@Bet Tn A O B)) (and (@InAngle Tn P A O B) (@CongA Tn A O P B O P))), @SAMS Tn A O P A O P *)
  intros P A O B H.
(* Goal: @SumA Tn A' O' B' A' O' B' A O B *)
  spliter.
(* Goal: @SumA Tn D E F D E F D' E' F' *)
  assert_diffs.
(* Goal: @SumA Tn A O P A O P A O B *)
  apply (conga3_suma__suma A O P B O P A O B); [SumA|CongA..].
Qed.

Lemma halfa_exists : forall A O B, ~ Bet A O B -> exists P, HalfA P A O B.
Proof.
(* Goal: forall (A O B : @Tpoint Tn) (_ : not (@Bet Tn A O B)), @ex (@Tpoint Tn) (fun P : @Tpoint Tn => HalfA P A O B) *)
  intros A O B HNBet.
(* Goal: @SumA Tn D E F D E F D' E' F' *)
  assert_diffs.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => HalfA P A O B) *)
  destruct (angle_bisector A O B) as [P [HIn HConga]]; auto.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => HalfA P A O B) *)
  apply conga_comm in HConga.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => HalfA P A O B) *)
  exists P; repeat (split; trivial).
Qed.

Lemma halfa_sym : forall A O B P, HalfA P A O B -> HalfA P B O A.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : HalfA A B C D), @Coplanar Tn A B C D *)
  unfold HalfA.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : and (not (@Bet Tn B C D)) (and (@InAngle Tn A B C D) (@CongA Tn B C A D C A))), @Coplanar Tn A B C D *)
  intros.
(* Goal: @SumA Tn A' O' B' A' O' B' A O B *)
  spliter.
(* Goal: HalfA M A O A' *)
  split; [|split].
(* Goal: not (@Bet Tn B O A) *)
(* Goal: @InAngle Tn P B O A *)
(* Goal: @CongA Tn B O P A O P *)
    intro; Between.
(* Goal: @InAngle Tn P B O A *)
(* Goal: @CongA Tn B O P A O P *)
    apply l11_24; assumption.
(* Goal: @CongA Tn A B P X Y Z *)
(* Goal: @CongA Tn X Y Z A' B' P' *)
    apply conga_sym; assumption.
Qed.

Lemma halfa__nbet : forall A O B P, HalfA P A O B -> ~ Bet A O P.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : HalfA A B C D), @Coplanar Tn A B C D *)
  unfold HalfA.
(* Goal: forall (A O B P : @Tpoint Tn) (_ : and (not (@Bet Tn A O B)) (and (@InAngle Tn P A O B) (@CongA Tn A O P B O P))), not (@Bet Tn A O P) *)
  intros A O B P H.
(* Goal: @SumA Tn A' O' B' A' O' B' A O B *)
  spliter.
(* Goal: not (@Bet Tn A O P) *)
  intro HBet.
(* Goal: False *)
  apply (not_bet_and_out A O P).
(* Goal: and (@Acute Tn D E F) (@SumA Tn D E F D E F D' E' F') *)
  split.
(* Goal: @CongA Tn X Y Z A B P *)
(* Goal: @CongA Tn A B P X' Y' Z' *)
    assumption.
(* Goal: @Out Tn O M P *)
  apply in_angle_out with B; trivial.
(* Goal: @SumA Tn D E F D E F D' E' F' *)
  assert_diffs.
(* Goal: @Out Tn O A B *)
  apply l6_2 with P; auto.
(* Goal: @CongA Tn X Y Z A B P *)
(* Goal: @CongA Tn A B P X' Y' Z' *)
  apply (bet_conga__bet A O P); assumption.
Qed.

Lemma out_preserves_halfa : forall P A O B P' A' B', 
 Out O A A' -> Out O B B' -> Out O P P' ->
 HalfA P A O B -> HalfA P' A' O B'.
Proof.
(* Goal: forall (P A O B P' A' B' : @Tpoint Tn) (_ : @Out Tn O A A') (_ : @Out Tn O B B') (_ : @Out Tn O P P') (_ : HalfA P A O B), HalfA P' A' O B' *)
  intros P A O B P' A' B' HA HB HP [HNBet []].
(* Goal: HalfA P' A' O B' *)
  apply l6_6 in HA.
(* Goal: HalfA P' A' O B' *)
  apply l6_6 in HB.
(* Goal: HalfA P' A' O B' *)
  apply l6_6 in HP.
(* Goal: HalfA M A O A' *)
  split; [|split].
(* Goal: @CongA Tn X Y Z A B P *)
(* Goal: @CongA Tn A B P X' Y' Z' *)
    intro; apply HNBet, bet_out_out_bet with A' B'; assumption.
(* Goal: @CongA Tn X Y Z A B P *)
(* Goal: @CongA Tn A B P X' Y' Z' *)
    apply l11_25 with P A B; assumption.
(* Goal: @CongA Tn X Y Z A B P *)
(* Goal: @CongA Tn A B P X' Y' Z' *)
    apply l11_10 with A P B P; assumption.
Qed.

Lemma halfa__nbet2 : forall A O B P, HalfA P A O B -> ~ Bet A O P /\ ~ Bet B O P.
Proof.
(* Goal: forall (A O B P : @Tpoint Tn) (_ : HalfA P A O B), and (not (@Bet Tn A O P)) (not (@Bet Tn B O P)) *)
  intros A O B P.
(* Goal: and (@Acute Tn D E F) (@SumA Tn D E F D E F D' E' F') *)
  split.
(* Goal: not (@Bet Tn A O P) *)
(* Goal: not (@Bet Tn B O P) *)
  apply (halfa__nbet A O B P); auto.
(* Goal: not (@Bet Tn B O P) *)
  apply halfa_sym in H.
(* Goal: not (@Bet Tn B O P) *)
  apply (halfa__nbet B O A P); auto.
Qed.


Lemma halfa_chara1 : forall P A O B, HalfA P A O B -> 
  exists A', exists M, Cong O A' O A /\ Out O A' B /\ Midpoint M A A' /\ Out O M P.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : HalfA A B C D), @Coplanar Tn A B C D *)
  unfold HalfA.
(* Goal: forall (P A O B : @Tpoint Tn) (_ : and (not (@Bet Tn A O B)) (and (@InAngle Tn P A O B) (@CongA Tn A O P B O P))), @SAMS Tn A O P A O P *)
  intros P A O B H.
(* Goal: @SumA Tn A' O' B' A' O' B' A O B *)
  spliter.
(* Goal: @SumA Tn D E F D E F D' E' F' *)
  assert_diffs.
(* Goal: @ex (@Tpoint Tn) (fun A' : @Tpoint Tn => @ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Cong Tn O A' O A) (and (@Out Tn O A' B) (and (@Midpoint Tn M A A') (@Out Tn O M P))))) *)
  destruct (l6_11_existence O O A B) as [A' []]; auto.
(* Goal: @ex (@Tpoint Tn) (fun A' : @Tpoint Tn => @ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Cong Tn O A' O A) (and (@Out Tn O A' B) (and (@Midpoint Tn M A A') (@Out Tn O M P))))) *)
  destruct (midpoint_existence A A') as [M].
(* Goal: @ex (@Tpoint Tn) (fun A' : @Tpoint Tn => @ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Cong Tn O A' O A) (and (@Out Tn O A' B) (and (@Midpoint Tn M A A') (@Out Tn O M P))))) *)
  exists A', M.
(* Goal: and (@Acute Tn D E F) (@SumA Tn D E F D E F D' E' F') *)
  split.
(* Goal: @CongA Tn X Y Z A B P *)
(* Goal: @CongA Tn A B P X' Y' Z' *)
    assumption.
(* Goal: and (@Acute Tn D E F) (@SumA Tn D E F D E F D' E' F') *)
  split.
(* Goal: @CongA Tn X Y Z A B P *)
(* Goal: @CongA Tn A B P X' Y' Z' *)
    assumption.
(* Goal: and (@Acute Tn D E F) (@SumA Tn D E F D E F D' E' F') *)
  split.
(* Goal: @CongA Tn X Y Z A B P *)
(* Goal: @CongA Tn A B P X' Y' Z' *)
    assumption.
(* Goal: @Out Tn O M P *)
  destruct (col_dec A O B) as [|HNCol].
(* Goal: @CongA Tn X Y Z A B P *)
(* Goal: @CongA Tn A B P X' Y' Z' *)
  { assert (Out O A B). apply not_bet_out; assumption.
(* Goal: @Out Tn O M P *)
    assert (A = A') by (apply (l6_11_uniqueness O O A B); Cong).
(* Goal: @Out Tn O M P *)
    treat_equalities.
(* Goal: @Out Tn O M P *)
    apply in_angle_out with B; trivial.
  }
(* Goal: @Out Tn O M P *)
  assert (InAngle M A O B).
(* Goal: @SumA Tn D E F D E F D' E' F' *)
  { assert_diffs.
(* Goal: @InAngle Tn M A O B *)
    assert (O <> M).
(* Goal: @InAngle Tn C' A' O B *)
(* Goal: @InAngle Tn C' A' O B *)
    { intro.
(* Goal: False *)
      subst M.
(* Goal: False *)
      absurd (Bet A O B); trivial.
(* Goal: @Bet Tn A O B *)
      apply between_symmetry, l6_2 with A'; Between.
    }
(* Goal: @InAngle Tn M A O B *)
    apply l11_25 with M A A'; [|apply out_trivial|apply l6_6|apply out_trivial]; auto.
(* Goal: and (not (@eq (@Tpoint Tn) O' A')) (and (not (@eq (@Tpoint Tn) O' B')) (and (not (@eq (@Tpoint Tn) O A)) (not (@eq (@Tpoint Tn) O B)))) *)
    repeat split; auto.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn A X A') (or (@eq (@Tpoint Tn) X O) (@Out Tn O X M))) *)
    exists M.
(* Goal: and (@Bet Tn A M A') (or (@eq (@Tpoint Tn) M O) (@Out Tn O M M)) *)
    split; Between.
(* Goal: or (@eq (@Tpoint Tn) M O) (@Out Tn O M M) *)
    right.
(* Goal: @Out Tn O A A *)
(* Goal: HalfA M A O A' *)
    apply out_trivial; auto.
  }
(* Goal: @Out Tn O M P *)
  apply col_inangle2__out with A B; trivial.
(* Goal: @Col Tn O M P *)
  apply conga2_cop2__col_1 with A B; [| |apply conga_comm; assumption|Cop..].
(* Goal: not (@Col Tn A O B) *)
(* Goal: @CongA Tn M O A M O B *)
    intro; destruct (or_bet_out A O B) as [|[|]]; auto.
(* Goal: @SumA Tn D E F D E F D' E' F' *)
  assert_diffs.
(* Goal: @CongA Tn M O A M O B *)
  destruct (l11_51 O M A O M A'); Cong.
(* Goal: not (@eq (@Tpoint Tn) M A) *)
(* Goal: @CongA Tn M O A M O B *)
    intro; treat_equalities; apply HNCol; Col.
(* Goal: @CongA Tn M O A M O B *)
  apply l11_10 with M A M A'; [|apply out_trivial..|apply l6_6]; auto.
Qed.

Lemma halfa_chara2 : forall P A O B,
  (exists A', exists M, Cong O A' O A /\ Out O A' B /\ Midpoint M A A' /\ Out O M P) -> HalfA P A O B.
Proof.
(* Goal: forall (P A O B : @Tpoint Tn) (_ : and (not (@Bet Tn A O B)) (and (@InAngle Tn P A O B) (@CongA Tn A O P B O P))), @SAMS Tn A O P A O P *)
  intros P A O B H.
(* Goal: HalfA P A O B *)
  destruct H as [A' [M [HCong [HOut [HM1 HM2]]]]].
(* Goal: @SumA Tn D E F D E F D' E' F' *)
  assert_diffs.
(* Goal: HalfA P A O B *)
  apply out_preserves_halfa with M A A'; trivial.
(* Goal: @Out Tn O A A *)
(* Goal: HalfA M A O A' *)
    apply out_trivial; auto.
(* Goal: HalfA M A O A' *)
  split; [|split].
(* Goal: not (@CongA Tn A' O' P' A O P) *)
  - intro.
(* Goal: False *)
    absurd (O = M); auto.
(* Goal: @eq (@Tpoint Tn) O M *)
    apply l7_17 with A A'; trivial.
(* Goal: @Midpoint Tn O A A' *)
    split; Cong.
(* Goal: and (not (@eq (@Tpoint Tn) O' A')) (and (not (@eq (@Tpoint Tn) O' B')) (and (not (@eq (@Tpoint Tn) O A)) (not (@eq (@Tpoint Tn) O B)))) *)
  - repeat split; auto.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn A X A') (or (@eq (@Tpoint Tn) X O) (@Out Tn O X M))) *)
    exists M.
(* Goal: and (@Acute Tn D E F) (@SumA Tn D E F D E F D' E' F') *)
    split.
(* Goal: not (@Bet Tn B O A) *)
(* Goal: @InAngle Tn P B O A *)
(* Goal: @CongA Tn B O P A O P *)
(* Goal: @CongA Tn A' O' B' B O P *)
      Between.
(* Goal: @Out Tn O A A *)
(* Goal: HalfA M A O A' *)
      right; apply out_trivial; auto.
  - destruct (eq_dec_points A A').
(* Goal: @CongA Tn A O M A' O M *)
(* Goal: @CongA Tn A O M A' O M *)
      subst; apply conga_refl; auto.
(* Goal: @SumA Tn D E F D E F D' E' F' *)
    assert_diffs.
(* Goal: @CongA Tn A O M A' O M *)
    destruct (l11_51 O A M O A' M); Cong.
Qed.

Lemma halfa_uniqueness : forall O A B P P', HalfA P A O B -> HalfA P' A O B -> Out O P P'.
Proof.
(* Goal: forall (O A B P P' : @Tpoint Tn) (_ : HalfA P A O B) (_ : HalfA P' A O B), @Out Tn O P P' *)
  intros O A B P P' HP HP'.
(* Goal: @Out Tn O P P' *)
  apply halfa_chara1 in HP.
(* Goal: @Out Tn O P P' *)
  apply halfa_chara1 in HP'.
(* Goal: @Out Tn O P P' *)
  destruct HP as [A1 [M1]].
(* Goal: @Out Tn O P P' *)
  destruct HP' as [A2 [M2]].
(* Goal: @SumA Tn A' O' B' A' O' B' A O B *)
  spliter.
(* Goal: @Out Tn O P P' *)
  assert (A1 = A2).
(* Goal: @SumA Tn D E F D E F D' E' F' *)
  { assert_diffs.
(* Goal: @eq (@Tpoint Tn) A1 A2 *)
    apply (l6_11_uniqueness O O A B); auto.
  }
(* Goal: @Out Tn O P P' *)
  subst A2.
(* Goal: @Out Tn O P P' *)
  assert(M1 = M2) by (apply (l7_17 A A1); assumption).
(* Goal: @Out Tn O P P' *)
  subst M2.
(* Goal: @CongA Tn X Y Z A B P *)
(* Goal: @CongA Tn A B P X' Y' Z' *)
  apply l6_7 with M1; [apply l6_6|]; assumption.
Qed.

Lemma halfa_not_null : forall P A O B, ~ Col A O B -> HalfA P A O B -> ~ Col A O P.
Proof.
(* Goal: forall (P A O B : @Tpoint Tn) (_ : not (@Col Tn A O B)) (_ : HalfA P A O B), not (@Col Tn A O P) *)
  intros P A O B HNCol [_ [HIn HConga]] HCol.
(* Goal: False *)
  assert (Col B O P).
(* Goal: @CongA Tn X Y Z A B P *)
(* Goal: @CongA Tn A B P X' Y' Z' *)
    apply (col_conga_col A O P); assumption.
(* Goal: False *)
  apply HNCol.
(* Goal: @SumA Tn D E F D E F D' E' F' *)
  assert_diffs.
(* Goal: @Col Tn A O B *)
  ColR.
Qed.

Lemma null_halfa__null : forall P A O B, Col A O B -> HalfA P A O B -> Out O A P.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : HalfA A B C D), @Coplanar Tn A B C D *)
  unfold HalfA.
(* Goal: forall (P A O B : @Tpoint Tn) (_ : @Col Tn A O B) (_ : and (not (@Bet Tn A O B)) (and (@InAngle Tn P A O B) (@CongA Tn A O P B O P))), @Out Tn O A P *)
  intros P A O B HCol H.
(* Goal: @SumA Tn A' O' B' A' O' B' A O B *)
  spliter.
(* Goal: @Out Tn O A P *)
  assert (Out O A B) by (apply not_bet_out; assumption).
(* Goal: @CongA Tn X Y Z A B P *)
(* Goal: @CongA Tn A B P X' Y' Z' *)
  apply(in_angle_out A O B P); assumption.
Qed.

Lemma halfa1123__out : forall A O B, HalfA A A O B -> Out O A B.
Proof.
(* Goal: forall (A O B : @Tpoint Tn) (_ : HalfA A A O B), @Out Tn O A B *)
  intros A O B [_ [_ HCongA]].
(* Goal: @Out Tn O A B *)
  apply eq_conga_out with A O; CongA.
Qed.

Lemma halfa3123__out : forall A O B, HalfA B A O B -> Out O A B.
Proof.
(* Goal: forall (A O B : @Tpoint Tn) (_ : gHalfA A O B A O B), @Out Tn O A B *)
  intros A O B HHalf.
(* Goal: @Out Tn O A B *)
  apply l6_6, halfa1123__out, halfa_sym, HHalf.
Qed.

Lemma halfa__sams : forall P A O B, HalfA P A O B -> SAMS A O P A O P.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : HalfA A B C D), @Coplanar Tn A B C D *)
  unfold HalfA.
(* Goal: forall (P A O B : @Tpoint Tn) (_ : and (not (@Bet Tn A O B)) (and (@InAngle Tn P A O B) (@CongA Tn A O P B O P))), @SAMS Tn A O P A O P *)
  intros P A O B H.
(* Goal: @SumA Tn A' O' B' A' O' B' A O B *)
  spliter.
(* Goal: @SumA Tn D E F D E F D' E' F' *)
  assert_diffs.
(* Goal: @SAMS Tn A O P A O P *)
  apply (conga2_sams__sams A O P P O B); [CongA..|SumA].
Qed.

Lemma halfa__acute : forall P A O B, HalfA P A O B -> Acute A O P.
Proof.
(* Goal: forall (P A O B : @Tpoint Tn) (_ : HalfA P A O B), @Acute Tn A O P *)
  intros P A O B HHalfa.
(* Goal: @Acute Tn A O P *)
  apply nbet_sams_suma__acute with A O B.
(* Goal: @CongA Tn X Y Z A B P *)
(* Goal: @CongA Tn A B P X' Y' Z' *)
    destruct HHalfa; assumption.
(* Goal: @CongA Tn X Y Z A B P *)
(* Goal: @CongA Tn A B P X' Y' Z' *)
    apply halfa__sams with B; assumption.
(* Goal: @CongA Tn X Y Z A B P *)
(* Goal: @CongA Tn A B P X' Y' Z' *)
    apply halfa__suma; assumption.
Qed.

Lemma halfa__lea : forall P A O B, HalfA P A O B -> LeA A O P A O B.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : HalfA A B C D), @Coplanar Tn A B C D *)
  unfold HalfA.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : and (not (@Bet Tn B C D)) (and (@InAngle Tn A B C D) (@CongA Tn B C A D C A))), @Coplanar Tn A B C D *)
  intros.
(* Goal: @SumA Tn A' O' B' A' O' B' A O B *)
  spliter.
(* Goal: @CongA Tn X Y Z A B P *)
(* Goal: @CongA Tn A B P X' Y' Z' *)
  apply (inangle__lea); assumption.
Qed.

Lemma halfa2_lea__lea1 : forall P A O B P' A' O' B',
  HalfA P A O B -> HalfA P' A' O' B' -> LeA A' O' P' A O P -> LeA A' O' B' A O B.
Proof.
(* Goal: forall (P A O B P' A' O' B' : @Tpoint Tn) (_ : HalfA P A O B) (_ : HalfA P' A' O' B') (_ : @LeA Tn A' O' P' A O P), @LeA Tn A' O' B' A O B *)
  intros P A O B P' A' O' B' HP HP' HLea.
(* Goal: @LeA Tn A' O' B' A O B *)
  apply sams_lea2_suma2__lea with A' O' P' A' O' P' A O P A O P; trivial.
(* Goal: @CongA Tn X Y Z A B P *)
(* Goal: @CongA Tn A B P X' Y' Z' *)
    apply halfa__sams with B; assumption.
(* Goal: @CongA Tn X Y Z A B P *)
(* Goal: @CongA Tn A B P X' Y' Z' *)
    apply halfa__suma; assumption.
(* Goal: @CongA Tn X Y Z A B P *)
(* Goal: @CongA Tn A B P X' Y' Z' *)
    apply halfa__suma; assumption.
Qed.

Lemma halfa__ts : forall P A O B, ~ Col A O B -> HalfA P A O B -> TS O P A B.
Proof.
(* Goal: forall (P A O B : @Tpoint Tn) (_ : not (@Col Tn A O B)) (_ : HalfA P A O B), @TS Tn O P A B *)
  intros P A O B HNCol HHalfa.
(* Goal: @TS Tn O P A B *)
  assert(~ Col A O P) by (apply halfa_not_null with B; assumption).
(* Goal: @TS Tn O P A B *)
  assert(~ Col B O P).
(* Goal: not (@Col Tn B O P) *)
(* Goal: @TS Tn O P A B *)
    apply halfa_not_null with A; Col.
(* Goal: @CongA Tn X Y Z A B P *)
(* Goal: @CongA Tn A B P X' Y' Z' *)
    apply halfa_sym; assumption.
(* Goal: @TS Tn O P A B *)
  destruct HHalfa as [_ []].
(* Goal: @TS Tn O P A B *)
  apply invert_two_sides, in_angle_two_sides; Col.
Qed.

Lemma conga_halfa__conga1 : forall P A O B P' A' O' B', 
 HalfA P A O B -> HalfA P' A' O' B' ->
 CongA A O P A' O' P' -> 
 CongA A O B A' O' B'.
Proof.
(* Goal: forall (P A O B P' A' O' B' : @Tpoint Tn) (_ : HalfA P A O B) (_ : HalfA P' A' O' B') (_ : @CongA Tn A O B A' O' B'), @CongA Tn A O P A' O' P' *)
  intros P A O B P' A' O' B' HP HP' HConga.
(* Goal: @CongA Tn A O B A' O' B' *)
  apply (suma2__conga A O P A O P).
(* Goal: @CongA Tn X Y Z A B P *)
(* Goal: @CongA Tn A B P X' Y' Z' *)
    apply halfa__suma; assumption.
(* Goal: @SumA Tn A O P A O P A' O' B' *)
  assert (Hd := HP').
(* Goal: @LeA Tn A' O' P' A O P *)
  apply halfa_distincts in Hd.
(* Goal: @SumA Tn A' O' B' A' O' B' A O B *)
  spliter.
(* Goal: @SumA Tn A O P A O P A' O' B' *)
  apply (conga3_suma__suma A' O' P' A' O' P' A' O' B'); [|CongA..].
(* Goal: @CongA Tn X Y Z A B P *)
(* Goal: @CongA Tn A B P X' Y' Z' *)
  apply halfa__suma; assumption.
Qed.

Lemma conga_halfa__conga2 : forall P A O B P' A' O' B', 
 HalfA P A O B -> HalfA P' A' O' B' -> CongA A O B A' O' B' -> CongA A O P A' O' P'.
Proof.
(* Goal: forall (P A O B P' A' O' B' : @Tpoint Tn) (_ : HalfA P A O B) (_ : HalfA P' A' O' B') (_ : @CongA Tn A O B A' O' B'), @CongA Tn A O P A' O' P' *)
  intros P A O B P' A' O' B' HP HP' HConga.
(* Goal: @CongA Tn A O P A' O' P' *)
  apply sams2_suma2__conga with A O B.
(* Goal: @CongA Tn X Y Z A B P *)
(* Goal: @CongA Tn A B P X' Y' Z' *)
    apply halfa__sams with B; assumption.
(* Goal: @CongA Tn X Y Z A B P *)
(* Goal: @CongA Tn A B P X' Y' Z' *)
    apply halfa__suma; assumption.
(* Goal: @CongA Tn X Y Z A B P *)
(* Goal: @CongA Tn A B P X' Y' Z' *)
    apply halfa__sams with B'; assumption.
(* Goal: @SumA Tn A' O' P' A' O' P' A O B *)
  apply halfa__suma in HP'.
(* Goal: @SumA Tn D E F D E F D' E' F' *)
  assert_diffs.
(* Goal: @SumA Tn A' O' P' A' O' P' A O B *)
  apply (conga3_suma__suma A' O' P' A' O' P' A' O' B'); CongA.
Qed.

Lemma halfa2_lta__lta1 : forall P A O B P' A' O' B',
  HalfA P A O B -> HalfA P' A' O' B' -> LtA A' O' P' A O P -> LtA A' O' B' A O B.
Proof.
(* Goal: forall (P A O B P' A' O' B' : @Tpoint Tn) (_ : HalfA P A O B) (_ : HalfA P' A' O' B') (_ : @LtA Tn A' O' B' A O B), @LtA Tn A' O' P' A O P *)
  intros P A O B P' A' O' B' HP HP' [HLea HNCong].
(* Goal: and (@Acute Tn D E F) (@SumA Tn D E F D E F D' E' F') *)
  split.
(* Goal: @CongA Tn X Y Z A B P *)
(* Goal: @CongA Tn A B P X' Y' Z' *)
    apply halfa2_lea__lea1 with P P'; assumption.
(* Goal: not (@CongA Tn A' O' P' A O P) *)
  intro.
(* Goal: False *)
  apply HNCong.
(* Goal: @CongA Tn X Y Z A B P *)
(* Goal: @CongA Tn A B P X' Y' Z' *)
  apply conga_halfa__conga2 with B' B; assumption.
Qed.

Lemma halfa2_lea__lea2 : forall P A O B P' A' O' B',
  HalfA P A O B -> HalfA P' A' O' B' -> LeA A' O' B' A O B -> LeA A' O' P' A O P.
Proof.
(* Goal: forall (P A O B P' A' O' B' : @Tpoint Tn) (_ : HalfA P A O B) (_ : HalfA P' A' O' B') (_ : @LeA Tn A' O' B' A O B), @LeA Tn A' O' P' A O P *)
  intros P A O B P' A' O' B' HP HP' HLeA.
(* Goal: @LeA Tn A' O' P' A O P *)
  assert (Hd := HP).
(* Goal: @LeA Tn A' O' P' A O P *)
  apply halfa_distincts in Hd.
(* Goal: @LeA Tn A' O' P' A O P *)
  assert (Hd' := HP').
(* Goal: @LeA Tn A' O' P' A O P *)
  apply halfa_distincts in Hd'.
(* Goal: @SumA Tn A' O' B' A' O' B' A O B *)
  spliter.
(* Goal: @LeA Tn A' O' P' A O P *)
  destruct (lea_total A O P A' O' P'); auto.
(* Goal: @LeA Tn A' O' P' A O P *)
  apply conga__lea.
(* Goal: @CongA Tn X Y Z A B P *)
(* Goal: @CongA Tn A B P X' Y' Z' *)
  apply conga_halfa__conga2 with B' B; [assumption..|].
(* Goal: @CongA Tn A' O' B' A O B *)
  apply lea_asym; [assumption|].
(* Goal: @CongA Tn X Y Z A B P *)
(* Goal: @CongA Tn A B P X' Y' Z' *)
  apply halfa2_lea__lea1 with P' P; assumption.
Qed.

Lemma halfa2_lta__lta2 : forall P A O B P' A' O' B',
  HalfA P A O B -> HalfA P' A' O' B' -> LtA A' O' B' A O B -> LtA A' O' P' A O P.
Proof.
(* Goal: forall (P A O B P' A' O' B' : @Tpoint Tn) (_ : HalfA P A O B) (_ : HalfA P' A' O' B') (_ : @LtA Tn A' O' B' A O B), @LtA Tn A' O' P' A O P *)
  intros P A O B P' A' O' B' HP HP' [HLea HNCong].
(* Goal: and (@Acute Tn D E F) (@SumA Tn D E F D E F D' E' F') *)
  split.
(* Goal: @CongA Tn X Y Z A B P *)
(* Goal: @CongA Tn A B P X' Y' Z' *)
    apply halfa2_lea__lea2 with B B'; assumption.
(* Goal: not (@CongA Tn A' O' P' A O P) *)
  intro.
(* Goal: False *)
  apply HNCong.
(* Goal: @CongA Tn X Y Z A B P *)
(* Goal: @CongA Tn A B P X' Y' Z' *)
  apply conga_halfa__conga1 with P' P; assumption.
Qed.

Lemma col_halfa__out : forall P A O B, Col A O B -> HalfA P A O B -> Out O A B.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : HalfA A B C D), @Coplanar Tn A B C D *)
  unfold HalfA.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : and (not (@Bet Tn B C D)) (and (@InAngle Tn A B C D) (@CongA Tn B C A D C A))), @Coplanar Tn A B C D *)
  intros.
(* Goal: @SumA Tn A' O' B' A' O' B' A O B *)
  spliter.
(* Goal: @CongA Tn X Y Z A B P *)
(* Goal: @CongA Tn A B P X' Y' Z' *)
  apply not_bet_out; assumption.
Qed.

(*
Lemma lta_nbet__ncol : forall A B C X Y Z, ~ Bet X Y Z -> LtA A B C X Y Z -> ~ Col X Y Z.
Proof.
  intros A B C X Y Z HNBet HLta HCol.
  apply HNBet.
(* Goal: @CongA Tn X Y Z A B P *)
(* Goal: @CongA Tn A B P X' Y' Z' *)
  apply (col_lta__bet A B C); assumption.
Qed.
*)

Lemma halfa__coplanar : forall A B C D, 
  HalfA A B C D -> Coplanar A B C D.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : HalfA A B C D), @Coplanar Tn A B C D *)
  unfold HalfA.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : and (not (@Bet Tn B C D)) (and (@InAngle Tn A B C D) (@CongA Tn B C A D C A))), @Coplanar Tn A B C D *)
  intros.
(* Goal: @SumA Tn A' O' B' A' O' B' A O B *)
  spliter.
(* Goal: @CongA Tn X Y Z A B P *)
(* Goal: @CongA Tn A B P X' Y' Z' *)
  apply inangle__coplanar; assumption.
Qed.

Lemma cop_halfa_perp__os : forall P A O B T, HalfA P A O B -> Perp O P T O -> Coplanar A O P T ->
  OS O T P A.
Proof.
(* Goal: forall (P A O B T : @Tpoint Tn) (_ : HalfA P A O B) (_ : @Perp Tn O P T O) (_ : @Coplanar Tn A O P T), and (@OS Tn O T P A) (@OS Tn O T P B) *)
  intros P A O B T HP HPerp HCop.
(* Goal: @OS Tn O T P A *)
  apply acute_cop_perp__one_side.
(* Goal: @CongA Tn X Y Z A B P *)
(* Goal: @CongA Tn A B P X' Y' Z' *)
    apply acute_sym, halfa__acute with B; assumption.
(* Goal: @CongA Tn X Y Z A B P *)
(* Goal: @CongA Tn A B P X' Y' Z' *)
    assumption.
(* Goal: @Coplanar Tn P T O A *)
    Cop.
Qed.

Lemma cop_halfa_perp__os2 : forall P A O B T, HalfA P A O B -> Perp O P T O -> Coplanar A O P T ->
  OS O T P A /\ OS O T P B.
Proof.
(* Goal: forall (P A O B T : @Tpoint Tn) (_ : HalfA P A O B) (_ : @Perp Tn O P T O) (_ : @Coplanar Tn A O P T), and (@OS Tn O T P A) (@OS Tn O T P B) *)
  intros P A O B T HP HPerp HCop.
(* Goal: and (@Acute Tn D E F) (@SumA Tn D E F D E F D' E' F') *)
  split.
(* Goal: @CongA Tn X Y Z A B P *)
(* Goal: @CongA Tn A B P X' Y' Z' *)
    apply cop_halfa_perp__os with B; assumption.
(* Goal: @OS Tn O T P B *)
  apply cop_halfa_perp__os with A.
(* Goal: @CongA Tn X Y Z A B P *)
(* Goal: @CongA Tn A B P X' Y' Z' *)
    apply halfa_sym; assumption.
(* Goal: @CongA Tn X Y Z A B P *)
(* Goal: @CongA Tn A B P X' Y' Z' *)
    assumption.
(* Goal: @Coplanar Tn B O P T *)
  destruct (col_dec A O P).
(* Goal: @InAngle Tn C' A' O B *)
(* Goal: @InAngle Tn C' A' O B *)
  { assert (Col B O P); [|Cop].
(* Goal: @Col Tn B O P *)
    destruct HP as [_ []].
(* Goal: @CongA Tn X Y Z A B P *)
(* Goal: @CongA Tn A B P X' Y' Z' *)
    apply (col_conga_col A O P); assumption.
  }
(* Goal: @Coplanar Tn B O P T *)
  apply halfa__coplanar in HP.
(* Goal: @Coplanar Tn P T O A *)
  apply coplanar_perm_12, coplanar_trans_1 with A; Cop.
Qed.

Lemma inangle_halfa2__inangle : forall O A B C A' C',
  ~ Col A O B -> InAngle C A O B ->
  HalfA A' A O B -> HalfA C' C O B ->
  InAngle C' A' O B.
Proof.
(* Goal: forall (O A B C A' C' : @Tpoint Tn) (_ : not (@Col Tn A O B)) (_ : @InAngle Tn C A O B) (_ : HalfA A' A O B) (_ : HalfA C' C O B), @InAngle Tn C' A' O B *)
  intros O A B C A' C' HNCol HC HA' HC'.
(* Goal: @InAngle Tn C' A' O B *)
  apply halfa_sym in HA'.
(* Goal: @InAngle Tn C' A' O B *)
  apply halfa_sym in HC'.
(* Goal: @InAngle Tn C' A' O B *)
  destruct (col_dec B O C).
(* Goal: @InAngle Tn C' A' O B *)
(* Goal: @InAngle Tn C' A' O B *)
  { apply out341__inangle.
(* Goal: not (@eq (@Tpoint Tn) A' O) *)
(* Goal: @Out Tn O B C' *)
      apply halfa_distincts in HA'; spliter; auto.
(* Goal: @CongA Tn X Y Z A B P *)
(* Goal: @CongA Tn A B P X' Y' Z' *)
    apply null_halfa__null with C; assumption.
  }
(* Goal: @InAngle Tn C' A' O B *)
  apply l11_24, lea_in_angle.
(* Goal: @CongA Tn X Y Z A B P *)
(* Goal: @CongA Tn A B P X' Y' Z' *)
    apply halfa2_lea__lea2 with A C; [assumption..|].
(* Goal: @LeA Tn B O C B O A *)
(* Goal: @OS Tn B O A' C' *)
    apply inangle__lea, l11_24, HC.
  apply one_side_transitivity with A; [|apply one_side_transitivity with C; apply one_side_symmetry];
    apply in_angle_one_side; Col.
(* Goal: not (@Col Tn O B A') *)
(* Goal: @InAngle Tn A' B O A *)
(* Goal: @InAngle Tn C B O A *)
(* Goal: not (@Col Tn O B C') *)
(* Goal: @InAngle Tn C' B O C *)
    apply halfa_not_null in HA'; Col.
(* Goal: @CongA Tn X Y Z A B P *)
(* Goal: @CongA Tn A B P X' Y' Z' *)
    destruct HA' as [_ []]; assumption.
(* Goal: @InAngle Tn C B O A *)
(* Goal: not (@Col Tn O B C') *)
(* Goal: @InAngle Tn C' B O C *)
    apply l11_24, HC.
(* Goal: not (@Col Tn O B C') *)
(* Goal: @InAngle Tn C' B O C *)
    apply halfa_not_null in HC'; Col.
(* Goal: @InAngle Tn C' B O C *)
    destruct HC' as [_ []]; Col.
Qed.

Definition gHalfA A' O' B' A O B := exists P, HalfA P A O B /\ CongA A' O' B' A O P.

Lemma ghalfa_distincts : forall A' O' B' A O B, gHalfA A' O' B' A O B ->
  O' <> A' /\ O' <> B' /\ O <> A /\ O <> B.
Proof.
(* Goal: forall (A' O' B' A O B : @Tpoint Tn) (_ : gHalfA A' O' B' A O B), gHalfA B' O' A' A O B *)
  intros A' O' B' A O B [P [HP]].
(* Goal: @CongA Tn A O P A O P *)
  apply halfa_distincts in HP.
(* Goal: @SumA Tn A' O' B' A' O' B' A O B *)
  spliter.
(* Goal: @SumA Tn D E F D E F D' E' F' *)
  assert_diffs.
(* Goal: and (not (@eq (@Tpoint Tn) O' A')) (and (not (@eq (@Tpoint Tn) O' B')) (and (not (@eq (@Tpoint Tn) O A)) (not (@eq (@Tpoint Tn) O B)))) *)
  repeat split; auto.
Qed.

Lemma halfa__ghalfa : forall P A O B, HalfA P A O B -> gHalfA A O P A O B.
Proof.
(* Goal: forall (P A O B : @Tpoint Tn) (_ : HalfA P A O B), gHalfA A O P A O B *)
  intros P A O B HP.
(* Goal: gHalfA A' O' B' B O A *)
  exists P.
(* Goal: and (HalfA P A O B) (@CongA Tn A O P A O P) *)
  split; [assumption|].
(* Goal: @CongA Tn A O P A O P *)
  apply halfa_distincts in HP.
(* Goal: @SumA Tn A' O' B' A' O' B' A O B *)
  spliter.
(* Goal: @CongA Tn A O P A O P *)
  apply conga_refl; auto.
Qed.

Lemma ghalfa_left_comm : forall A' O' B' A O B, gHalfA A' O' B' A O B ->
  gHalfA B' O' A' A O B.
Proof.
(* Goal: forall (A' O' B' A O B : @Tpoint Tn) (_ : gHalfA A' O' B' A O B), gHalfA B' O' A' A O B *)
  intros A' O' B' A O B [P [HP]].
(* Goal: gHalfA A' O' B' B O A *)
  exists P.
(* Goal: and (HalfA P A O B) (@CongA Tn B' O' A' A O P) *)
  split; CongA.
Qed.

Lemma ghalfa_right_comm : forall A' O' B' A O B, gHalfA A' O' B' A O B ->
  gHalfA A' O' B' B O A.
Proof.
(* Goal: forall (A' O' B' A O B : @Tpoint Tn) (_ : gHalfA A' O' B' A O B), gHalfA A' O' B' B O A *)
  intros A' O' B' A O B [P [[HNBet [HP1 HP2]] HP3]].
(* Goal: gHalfA A' O' B' B O A *)
  exists P.
(* Goal: and (HalfA P B O A) (@CongA Tn A' O' B' B O P) *)
  split; [split; [|split]|].
(* Goal: not (@Bet Tn B O A) *)
(* Goal: @InAngle Tn P B O A *)
(* Goal: @CongA Tn B O P A O P *)
(* Goal: @CongA Tn A' O' B' B O P *)
    Between.
(* Goal: @InAngle Tn P B O A *)
(* Goal: @CongA Tn B O P A O P *)
(* Goal: @CongA Tn A' O' B' B O P *)
    apply l11_24, HP1.
(* Goal: @CongA Tn B O P A O P *)
(* Goal: @CongA Tn A' O' B' B O P *)
    CongA.
(* Goal: @CongA Tn X Y Z A B P *)
(* Goal: @CongA Tn A B P X' Y' Z' *)
    apply conga_trans with A O P; assumption.
Qed.

Lemma ghalfa_comm : forall A' O' B' A O B, gHalfA A' O' B' A O B ->
  gHalfA B' O' A' B O A.
Proof.
(* Goal: forall (A' O' B' A O B : @Tpoint Tn) (_ : gHalfA A' O' B' A O B), gHalfA B' O' A' B O A *)
  intros A' O' B' A O B H.
(* Goal: gHalfA B' O' A' B O A *)
  apply ghalfa_left_comm, ghalfa_right_comm, H.
Qed.

Lemma ghalfa_exists : forall A O B, ~ Bet A O B -> exists A' O' B', gHalfA A' O' B' A O B.
Proof.
(* Goal: forall (A O B : @Tpoint Tn) (_ : not (@Bet Tn A O B)), @ex (@Tpoint Tn) (fun A' : @Tpoint Tn => @ex (@Tpoint Tn) (fun O' : @Tpoint Tn => @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => gHalfA A' O' B' A O B))) *)
  intros A O B H.
(* Goal: @ex (@Tpoint Tn) (fun A' : @Tpoint Tn => @ex (@Tpoint Tn) (fun O' : @Tpoint Tn => @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => gHalfA A' O' B' A O B))) *)
  destruct (halfa_exists A O B H) as [P HP].
(* Goal: @ex (@Tpoint Tn) (fun A' : @Tpoint Tn => @ex (@Tpoint Tn) (fun O' : @Tpoint Tn => @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => gHalfA A' O' B' A O B))) *)
  exists A, O, P.
(* Goal: gHalfA A O P A O B *)
  apply halfa__ghalfa, HP.
Qed.


Lemma ghalfa__suma : forall A' O' B' A O B, gHalfA A' O' B' A O B ->
  SumA A' O' B' A' O' B' A O B.
Proof.
(* Goal: forall (A' O' B' A O B : @Tpoint Tn) (_ : gHalfA A' O' B' A O B), @Acute Tn A' O' B' *)
  intros A' O' B' A O B [P [HHalf HConga]].
(* Goal: @SumA Tn A' O' B' A' O' B' A O B *)
  assert (Hd := HHalf).
(* Goal: @SumA Tn A' O' B' A' O' B' A O B *)
  apply halfa_distincts in HHalf.
(* Goal: @SumA Tn A' O' B' A' O' B' A O B *)
  spliter.
(* Goal: @CongA Tn B O P A O P *)
(* Goal: @CongA Tn A' O' B' B O P *)
  apply (conga3_suma__suma A O P A O P A O B); [|CongA..].
(* Goal: @CongA Tn X Y Z A B P *)
(* Goal: @CongA Tn A B P X' Y' Z' *)
  apply halfa__suma; assumption.
Qed.

Lemma ghalfa__acute : forall A' O' B' A O B, gHalfA A' O' B' A O B ->
  Acute A' O' B'.
Proof.
(* Goal: forall (A' O' B' A O B : @Tpoint Tn) (_ : gHalfA A' O' B' A O B), @Acute Tn A' O' B' *)
  intros A' O' B' A O B [P [HHalf HConga]].
(* Goal: @CongA Tn B O P A O P *)
(* Goal: @CongA Tn A' O' B' B O P *)
  apply (acute_conga__acute A O P); CongA.
(* Goal: @Acute Tn A O P *)
  apply halfa__acute with B, HHalf.
Qed.

Lemma ghalfa_chara : forall A' O' B' A O B,
  gHalfA A' O' B' A O B <-> (Acute A' O' B' /\ SumA A' O' B' A' O' B' A O B).
Proof.
(* Goal: forall A' O' B' A O B : @Tpoint Tn, iff (gHalfA A' O' B' A O B) (and (@Acute Tn A' O' B') (@SumA Tn A' O' B' A' O' B' A O B)) *)
  intros A' O' B' A O B.
(* Goal: and (@Acute Tn D E F) (@SumA Tn D E F D E F D' E' F') *)
  split.
(* Goal: forall _ : gHalfA A' O' B' A O B, and (@Acute Tn A' O' B') (@SumA Tn A' O' B' A' O' B' A O B) *)
(* Goal: forall _ : and (@Acute Tn A' O' B') (@SumA Tn A' O' B' A' O' B' A O B), gHalfA A' O' B' A O B *)
    intro HHalf; split; [eapply ghalfa__acute, HHalf|apply ghalfa__suma, HHalf].
(* Goal: forall _ : and (@Acute Tn A B C) (@SumA Tn A B C A B C A' B' C'), and (@Acute Tn D E F) (@SumA Tn D E F D E F D' E' F') *)
  intros [HAcute HSuma].
(* Goal: gHalfA A' O' B' A O B *)
  destruct (halfa_exists A O B) as [P HP].
(* Goal: @CongA Tn X Y Z A B P *)
(* Goal: @CongA Tn A B P X' Y' Z' *)
    apply (acute_suma__nbet A' O' B'); assumption.
(* Goal: and (HalfA P A O B) (@CongA Tn A O P A O P) *)
  exists P; split; [assumption|].
(* Goal: @CongA Tn A' O' B' A O P *)
  apply sams2_suma2__conga with A O B; [SumA..| |].
(* Goal: @SAMS Tn A O P A O P *)
(* Goal: @SumA Tn A O P A O P A O B *)
    eapply halfa__sams, HP.
(* Goal: @SumA Tn A O P A O P A O B *)
    apply halfa__suma, HP.
Qed.

Lemma ghalfa__out : forall A O B, gHalfA A O B A O B -> Out O A B.
Proof.
(* Goal: forall (A O B : @Tpoint Tn) (_ : gHalfA A O B A O B), @Out Tn O A B *)
  intros A O B HHalf.
(* Goal: @SumA Tn A' O' B' A' O' B' A O B *)
  rewrite ghalfa_chara in HHalf; spliter.
(* Goal: @Out Tn O A B *)
  apply (sams_suma__out546 A O B); SumA.
Qed.

Lemma ghalfa_preserves_lta : forall A B C X Y Z A' B' C' X' Y' Z',
  gHalfA A' B' C' A B C -> gHalfA X' Y' Z' X Y Z -> LtA A B C X Y Z -> LtA A' B' C' X' Y' Z'.
Proof.
(* Goal: forall (A B C X Y Z A' B' C' X' Y' Z' : @Tpoint Tn) (_ : gHalfA A' B' C' A B C) (_ : gHalfA X' Y' Z' X Y Z) (_ : @LtA Tn A B C X Y Z), @LtA Tn A' B' C' X' Y' Z' *)
  intros A B C X Y Z A' B' C' X' Y' Z' [P1 []] [P2 []] HLta.
(* Goal: @CongA Tn B O P A O P *)
(* Goal: @CongA Tn A' O' B' B O P *)
  apply (conga_preserves_lta A B P1 X Y P2); [CongA..|].
(* Goal: @CongA Tn X Y Z A B P *)
(* Goal: @CongA Tn A B P X' Y' Z' *)
  apply halfa2_lta__lta2 with Z C; assumption.
Qed.

(** Given two angles a and b, a/2 = b/2 -> a = b *)

Lemma ghalfa_preserves_conga_1 : forall A B C A' B' C' X Y Z X' Y' Z', 
  gHalfA X Y Z A B C -> gHalfA X' Y' Z' A' B' C' -> CongA X Y Z X' Y' Z' ->
  CongA A B C A' B' C'.
Proof.
(* Goal: forall (A B C A' B' C' X Y Z X' Y' Z' : @Tpoint Tn) (_ : gHalfA X Y Z A B C) (_ : gHalfA X' Y' Z' A' B' C') (_ : @CongA Tn A B C A' B' C'), @CongA Tn X Y Z X' Y' Z' *)
  intros A B C A' B' C' X Y Z X' Y' Z' [P []] [P' []] HConga.
(* Goal: @CongA Tn X Y Z A B P *)
(* Goal: @CongA Tn A B P X' Y' Z' *)
  apply conga_halfa__conga1 with P P'; [assumption..|].
(* Goal: @CongA Tn A B P A' B' P' *)
  apply conga_trans with X Y Z.
(* Goal: @CongA Tn A B P X Y Z *)
(* Goal: @CongA Tn X Y Z A' B' P' *)
    apply conga_sym; assumption.
(* Goal: @CongA Tn X Y Z A B P *)
(* Goal: @CongA Tn A B P X' Y' Z' *)
  apply conga_trans with X' Y' Z'; assumption.
Qed.

(** Given two angles a and b, a = b -> a/2 = b/2 *)

Lemma ghalfa_preserves_conga_2 : forall A B C A' B' C' X Y Z X' Y' Z',
  gHalfA X Y Z A B C -> gHalfA X' Y' Z' A' B' C' -> CongA A B C A' B' C' ->
  CongA X Y Z X' Y' Z'.
Proof.
(* Goal: forall (A B C A' B' C' X Y Z X' Y' Z' : @Tpoint Tn) (_ : gHalfA X Y Z A B C) (_ : gHalfA X' Y' Z' A' B' C') (_ : @CongA Tn A B C A' B' C'), @CongA Tn X Y Z X' Y' Z' *)
  intros A B C A' B' C' X Y Z X' Y' Z' [P []] [P' []] HConga.
(* Goal: @CongA Tn X Y Z X' Y' Z' *)
  apply conga_trans with A B P.
(* Goal: @CongA Tn X Y Z A B P *)
(* Goal: @CongA Tn A B P X' Y' Z' *)
    assumption.
(* Goal: @CongA Tn A B P X' Y' Z' *)
  apply conga_trans with A' B' P'; [|apply conga_sym; assumption].
(* Goal: @CongA Tn X Y Z A B P *)
(* Goal: @CongA Tn A B P X' Y' Z' *)
  apply conga_halfa__conga2 with C C'; assumption.
Qed.

(** Unicity of the double angle *)

Lemma ghalfa2__conga_1 : forall A B C A' B' C' A'' B'' C'',
  gHalfA A B C A' B' C' -> gHalfA A B C A'' B'' C'' -> CongA A' B' C' A'' B'' C''.
Proof.
(* Goal: forall (A B C A' B' C' A'' B'' C'' : @Tpoint Tn) (_ : gHalfA A B C A' B' C') (_ : gHalfA A B C A'' B'' C''), @CongA Tn A' B' C' A'' B'' C'' *)
  intros A B C A' B' C' A'' B'' C''.
(* Goal: forall _ : gHalfA A B C A' B' C', gHalfA D E F D' E' F' *)
  rewrite 2 ghalfa_chara.
(* Goal: forall (_ : and (@Acute Tn A B C) (@SumA Tn A B C A B C A' B' C')) (_ : and (@Acute Tn A B C) (@SumA Tn A B C A B C A'' B'' C'')), @CongA Tn A' B' C' A'' B'' C'' *)
  intros [HAcute' HSuma'] [HAcute'' HSuma''].
(* Goal: @CongA Tn X Y Z A B P *)
(* Goal: @CongA Tn A B P X' Y' Z' *)
  apply (suma2__conga A B C A B C); assumption.
Qed.

(** Unicity of the half angle *)

Lemma ghalfa2__conga_2 : forall A B C A' B' C' A'' B'' C'',
  gHalfA A' B' C' A B C -> gHalfA A'' B'' C'' A B C -> CongA A' B' C' A'' B'' C''.
Proof.
(* Goal: forall (A B C A' B' C' A'' B'' C'' : @Tpoint Tn) (_ : gHalfA A' B' C' A B C) (_ : gHalfA A'' B'' C'' A B C), @CongA Tn A' B' C' A'' B'' C'' *)
  intros A B C A' B' C' A'' B'' C'' [P' []] [P'' []].
(* Goal: @CongA Tn A' B' C' A'' B'' C'' *)
  apply conga_trans with A B P'; [assumption|].
(* Goal: @CongA Tn A B P' A'' B'' C'' *)
  apply conga_trans with A B P''; [|CongA].
(* Goal: @CongA Tn A B P' A B P'' *)
  apply out2__conga.
(* Goal: @Out Tn B A A *)
(* Goal: @Out Tn B P'' P' *)
    apply out_trivial; assert_diffs; auto.
(* Goal: @CongA Tn X Y Z A B P *)
(* Goal: @CongA Tn A B P X' Y' Z' *)
  apply halfa_uniqueness with A C; assumption.
Qed.

(** CongA preserves gHalfA *)

Lemma conga2_ghalfa__ghalfa : forall A B C A' B' C' D E F D' E' F',
  CongA A B C D E F -> CongA A' B' C' D' E' F' -> gHalfA A B C A' B' C' ->
  gHalfA D E F D' E' F'.
Proof.
(* Goal: forall (A B C A' B' C' D E F D' E' F' : @Tpoint Tn) (_ : @CongA Tn A B C D E F) (_ : @CongA Tn A' B' C' D' E' F') (_ : gHalfA A B C A' B' C'), gHalfA D E F D' E' F' *)
  intros A B C A' B' C' D E F D' E' F' HConga HConga1.
(* Goal: forall _ : gHalfA A B C A' B' C', gHalfA D E F D' E' F' *)
  rewrite 2 ghalfa_chara.
(* Goal: forall _ : and (@Acute Tn A B C) (@SumA Tn A B C A B C A' B' C'), and (@Acute Tn D E F) (@SumA Tn D E F D E F D' E' F') *)
  intros [HAcute HSuma].
(* Goal: and (@Acute Tn D E F) (@SumA Tn D E F D E F D' E' F') *)
  split.
(* Goal: @CongA Tn X Y Z A B P *)
(* Goal: @CongA Tn A B P X' Y' Z' *)
    apply (acute_conga__acute A B C); assumption.
(* Goal: @CongA Tn X Y Z A B P *)
(* Goal: @CongA Tn A B P X' Y' Z' *)
    apply (conga3_suma__suma A B C A B C A' B' C'); assumption.
Qed.

(** Out preserves gHalfA *)

Lemma ghalfa_out4__ghalfa : forall A B C D E F A' C' D' F',
  Out B A' A -> Out B C' C -> Out E D' D -> Out E F' F -> gHalfA A B C D E F ->
  gHalfA A' B C' D' E F'.
Proof.
(* Goal: forall (A B C D E F A' C' D' F' : @Tpoint Tn) (_ : @Out Tn B A' A) (_ : @Out Tn B C' C) (_ : @Out Tn E D' D) (_ : @Out Tn E F' F) (_ : gHalfA A B C D E F), gHalfA A' B C' D' E F' *)
  intros A B C D E F A' C' D' F' HA HC HE HF HHalf.
(* Goal: @CongA Tn X Y Z A B P *)
(* Goal: @CongA Tn A B P X' Y' Z' *)
  apply conga2_ghalfa__ghalfa with A B C D E F; [apply out2__conga..|]; assumption.
Qed.

(** Given two angles a and b such that a/2 + b/2 is acute, a/2 + b/2 = (a+b)/2 *)

Lemma suma_preserves_ghalfa : forall A B C D E F X Y Z A' B' C' D' E' F' X' Y' Z',
  Acute X Y Z ->
  SumA A B C D E F X Y Z -> SumA A' B' C' D' E' F' X' Y' Z' ->
  gHalfA A B C A' B' C' -> gHalfA D E F D' E' F' ->
  gHalfA X Y Z X' Y' Z'.
Proof.
(* Goal: forall (A B C D E F X Y Z A' B' C' D' E' F' X' Y' Z' : @Tpoint Tn) (_ : @Acute Tn X Y Z) (_ : @SumA Tn A B C D E F X Y Z) (_ : @SumA Tn A' B' C' D' E' F' X' Y' Z') (_ : gHalfA A B C A' B' C') (_ : gHalfA D E F D' E' F'), gHalfA X Y Z X' Y' Z' *)
  intros A B C D E F X Y Z A' B' C' D' E' F' X' Y' Z' HAcute HSuma HSuma'.
(* Goal: forall (_ : gHalfA A B C A' B' C') (_ : gHalfA X Y Z X' Y' Z'), gHalfA D E F D' E' F' *)
  rewrite 3 ghalfa_chara.
(* Goal: forall (_ : and (@Acute Tn A B C) (@SumA Tn A B C A B C A' B' C')) (_ : and (@Acute Tn X Y Z) (@SumA Tn X Y Z X Y Z X' Y' Z')), and (@Acute Tn D E F) (@SumA Tn D E F D E F D' E' F') *)
  intros [HAcute1 HSuma1] [HAcute2 HSuma2].
(* Goal: and (@Acute Tn D E F) (@SumA Tn D E F D E F D' E' F') *)
  split; [apply HAcute|].
(* Goal: @SumA Tn D E F D E F D' E' F' *)
  assert_diffs.
(* Goal: @CongA Tn D'' E'' F'' D' E' F' *)
  destruct (ex_suma A' B' C' D E F) as [G [H [I]]]; auto.
(* Goal: @CongA Tn D'' E'' F'' D' E' F' *)
  assert (SumA A B C X Y Z G H I) by (apply suma_assoc_1 with A B C D E F A' B' C'; SumA).
(* Goal: @SumA Tn X Y Z X Y Z X' Y' Z' *)
  apply suma_assoc_1 with A B C D E F G H I; [SumA..|].
(* Goal: @SumA Tn G H I D E F X' Y' Z' *)
  apply suma_assoc_2 with A' B' C' D E F D' E' F'; [|SumA..].
(* Goal: @SAMS Tn A' B' C' D E F *)
  apply sams_assoc_2 with A B C A B C X Y Z; SumA.
Qed.

(** Given two angles a and b, a/2 - b/2 = (a-b)/2 *)

Lemma acute_ghalfa2_sams_suma2__ghalfa456 : forall A B C D E F X Y Z A' B' C' D' E' F' X' Y' Z',
  SAMS A' B' C' D' E' F' -> Acute D E F ->
  SumA A B C D E F X Y Z -> SumA A' B' C' D' E' F' X' Y' Z' ->
  gHalfA A B C A' B' C' -> gHalfA X Y Z X' Y' Z' ->
  gHalfA D E F D' E' F'.
Proof.
(* Goal: forall (A B C D E F X Y Z A' B' C' D' E' F' X' Y' Z' : @Tpoint Tn) (_ : @SAMS Tn A' B' C' D' E' F') (_ : @Acute Tn D E F) (_ : @SumA Tn A B C D E F X Y Z) (_ : @SumA Tn A' B' C' D' E' F' X' Y' Z') (_ : gHalfA A B C A' B' C') (_ : gHalfA X Y Z X' Y' Z'), gHalfA D E F D' E' F' *)
  intros A B C D E F X Y Z A' B' C' D' E' F' X' Y' Z' HSams HAcute HSuma HSuma'.
(* Goal: forall (_ : gHalfA A B C A' B' C') (_ : gHalfA X Y Z X' Y' Z'), gHalfA D E F D' E' F' *)
  rewrite 3 ghalfa_chara.
(* Goal: forall (_ : and (@Acute Tn A B C) (@SumA Tn A B C A B C A' B' C')) (_ : and (@Acute Tn X Y Z) (@SumA Tn X Y Z X Y Z X' Y' Z')), and (@Acute Tn D E F) (@SumA Tn D E F D E F D' E' F') *)
  intros [HAcute1 HSuma1] [HAcute2 HSuma2].
(* Goal: and (@Acute Tn D E F) (@SumA Tn D E F D E F D' E' F') *)
  split; [apply HAcute|].
(* Goal: @SumA Tn D E F D E F D' E' F' *)
  assert_diffs.
(* Goal: @SumA Tn D E F D E F D' E' F' *)
  destruct (ex_suma D E F D E F) as [D'' [E'' [F'' HSuma3]]]; auto.
(* Goal: @CongA Tn A O P A O P *)
  apply (conga3_suma__suma D E F D E F D'' E'' F''); try apply conga_refl; auto.
(* Goal: @CongA Tn D'' E'' F'' D' E' F' *)
  destruct (ex_suma A' B' C' D E F) as [G [H [I]]]; auto.
(* Goal: @CongA Tn D'' E'' F'' D' E' F' *)
  assert (SumA A B C X Y Z G H I) by (apply suma_assoc_1 with A B C D E F A' B' C'; SumA).
(* Goal: @CongA Tn D'' E'' F'' D' E' F' *)
  assert (SAMS A' B' C' D E F) by (apply sams_assoc_2 with A B C A B C X Y Z; SumA).
(* Goal: @CongA Tn D'' E'' F'' D' E' F' *)
  apply sams2_suma2__conga456 with A' B' C' X' Y' Z'; trivial; clear dependent D'; clear dependent E'.
(* Goal: @SAMS Tn A' B' C' D'' E'' F'' *)
(* Goal: @SumA Tn A' B' C' D'' E'' F'' X' Y' Z' *)
    apply sams_assoc_1 with D E F D E F G H I; [..|apply sams_assoc_2 with X Y Z A B C X Y Z]; SumA.
(* Goal: @SumA Tn A' B' C' D'' E'' F'' X' Y' Z' *)
    apply suma_assoc_1 with D E F D E F G H I; [..|apply suma_assoc_2 with X Y Z A B C X Y Z]; SumA.
Qed.

Lemma acute_ghalfa2_sams_suma2__ghalfa123 : forall A B C D E F X Y Z A' B' C' D' E' F' X' Y' Z',
  SAMS A' B' C' D' E' F' -> Acute A B C ->
  SumA A B C D E F X Y Z -> SumA A' B' C' D' E' F' X' Y' Z' ->
  gHalfA D E F D' E' F' -> gHalfA X Y Z X' Y' Z' ->
  gHalfA A B C A' B' C'.
Proof.
(* Goal: forall (A B C D E F X Y Z A' B' C' D' E' F' X' Y' Z' : @Tpoint Tn) (_ : @SAMS Tn A' B' C' D' E' F') (_ : @Acute Tn A B C) (_ : @SumA Tn A B C D E F X Y Z) (_ : @SumA Tn A' B' C' D' E' F' X' Y' Z') (_ : gHalfA D E F D' E' F') (_ : gHalfA X Y Z X' Y' Z'), gHalfA A B C A' B' C' *)
  intros A B C D E F X Y Z A' B' C' D' E' F' X' Y' Z' HSams HAcute HSuma HSuma' HHalf1 HHalf2.
(* Goal: gHalfA A B C A' B' C' *)
  apply acute_ghalfa2_sams_suma2__ghalfa456 with D E F X Y Z D' E' F' X' Y' Z'; SumA.
Qed.

End HalfAngle.

Section HalfAngle_2D.

(* Goal: @InAngle Tn C' A' O B *)
(* Goal: @InAngle Tn C' A' O B *)
Context `{T2D:Tarski_2D}.

Lemma halfa_perp__os : forall P A O B T, HalfA P A O B -> Perp O P T O -> OS O T P A.
Proof.
(* Goal: forall (P A O B T : @Tpoint Tn) (_ : @HalfA Tn P A O B) (_ : @Perp Tn O P T O), and (@OS Tn O T P A) (@OS Tn O T P B) *)
  intros P A O B T HP HT.
(* Goal: and (@OS Tn O T P A) (@OS Tn O T P B) *)
  assert (HCop := all_coplanar A O P T).
(* Goal: @CongA Tn X Y Z A B P *)
(* Goal: @CongA Tn A B P X' Y' Z' *)
  apply cop_halfa_perp__os with B; assumption.
Qed.

Lemma halfa_perp__os2 : forall P A O B T, HalfA P A O B -> Perp O P T O ->
  OS O T P A /\ OS O T P B.
Proof.
(* Goal: forall (P A O B T : @Tpoint Tn) (_ : @HalfA Tn P A O B) (_ : @Perp Tn O P T O), and (@OS Tn O T P A) (@OS Tn O T P B) *)
  intros P A O B T HP HT.
(* Goal: and (@OS Tn O T P A) (@OS Tn O T P B) *)
  assert (HCop := all_coplanar A O P T).
(* Goal: @CongA Tn X Y Z A B P *)
(* Goal: @CongA Tn A B P X' Y' Z' *)
  apply cop_halfa_perp__os2; assumption.
Qed.

End HalfAngle_2D.