Require Export GeoCoq.Tarski_dev.Ch06_out_lines.

Section Sums.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

(** Existence of the sum *)

Lemma ex_sums : forall A B C D, exists E F, SumS A B C D E F.
Proof.
(* Goal: forall A B C D : @Tpoint Tn, @ex (@Tpoint Tn) (fun E : @Tpoint Tn => @ex (@Tpoint Tn) (fun F : @Tpoint Tn => @SumS Tn A B C D E F)) *)
  intros A B C D.
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => @ex (@Tpoint Tn) (fun F : @Tpoint Tn => @SumS Tn A B C D E F)) *)
  destruct (segment_construction A B C D) as [R [HR1 HR2]].
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => @ex (@Tpoint Tn) (fun F : @Tpoint Tn => @SumS Tn A B C D E F)) *)
  exists A, R, A, B, R.
(* Goal: and (@Bet Tn A B R) (and (@Cong Tn A B A B) (and (@Cong Tn B R C D) (@Cong Tn A R A R))) *)
  repeat split; Cong.
Qed.

(** Commutativity of the sum. *)

Lemma sums_sym : forall A B C D E F, SumS A B C D E F -> SumS C D A B E F.
Proof.
(* Goal: forall (A B C D E F : @Tpoint Tn) (_ : @SumS Tn A B C D E F), @Le Tn C D E F *)
  intros A B C D E F HSumS.
(* Goal: @Le Tn E F E' F' *)
  destruct HSumS as [P [Q [R [HBet [HCong1 [HCong2 HCong3]]]]]].
(* Goal: @SumS Tn C D A B E F *)
  exists R, Q, P.
(* Goal: and (@Bet Tn A B B) (and (@Cong Tn A B A B) (and (@Cong Tn B B C C) (@Cong Tn A B A B))) *)
  repeat split; Between; Cong.
Qed.

(** Unicity of the sum. *)

Lemma sums2__cong56 : forall A B C D E F E' F', SumS A B C D E F -> SumS A B C D E' F' ->
  Cong E F E' F'.
Proof.
(* Goal: forall (A B C D E F E' F' : @Tpoint Tn) (_ : @SumS Tn A B C D E F) (_ : @SumS Tn A B C D E' F'), @Cong Tn E F E' F' *)
  intros A B C D E F E' F' HSumS HSumS'.
(* Goal: @Le Tn E F E' F' *)
  destruct HSumS as [P [Q [R [HBet [HCong1 [HCong2 HCong3]]]]]].
(* Goal: @Le Tn E F E' F' *)
  destruct HSumS' as [P' [Q' [R' [HBet' [HCong1' [HCong2' HCong3']]]]]].
(* Goal: @Cong Tn E F E' F' *)
  apply cong_transitivity with P R; Cong.
(* Goal: @Cong Tn P R E' F' *)
  apply cong_transitivity with P' R'; trivial.
(* Goal: @Cong Tn P R P' R' *)
  apply l2_11 with Q Q'; trivial.
(* Goal: @Cong Tn P Q P' Q' *)
(* Goal: @Cong Tn Q R Q' R' *)
  apply cong_transitivity with A B; Cong.
(* Goal: @Cong Tn Q R Q' R' *)
  apply cong_transitivity with C D; Cong.
Qed.

(** Unicity of the difference of segments. *)

Lemma sums2__cong12 : forall A B C D E F A' B', SumS A B C D E F -> SumS A' B' C D E F ->
  Cong A B A' B'.
Proof.
(* Goal: forall (A B C D E F A' B' : @Tpoint Tn) (_ : @SumS Tn A B C D E F) (_ : @SumS Tn A' B' C D E F), @Cong Tn A B A' B' *)
  intros A B C D E F A' B' HSumS HSumS'.
(* Goal: @Le Tn E F E' F' *)
  destruct HSumS as [P [Q [R [HBet [HCong1 [HCong2 HCong3]]]]]].
(* Goal: @Le Tn E F E' F' *)
  destruct HSumS' as [P' [Q' [R' [HBet' [HCong1' [HCong2' HCong3']]]]]].
(* Goal: @Cong Tn A B A' B' *)
  apply cong_transitivity with P Q; Cong.
(* Goal: @Cong Tn P Q A' B' *)
  apply cong_transitivity with P' Q'; trivial.
(* Goal: @Cong Tn P Q P' Q' *)
  apply l4_3 with R R'; trivial.
(* Goal: @Cong Tn P R P' R' *)
(* Goal: @Cong Tn Q R Q' R' *)
  apply cong_transitivity with E F; Cong.
(* Goal: @Cong Tn Q R Q' R' *)
  apply cong_transitivity with C D; Cong.
Qed.

(** Unicity of the difference of segments on the right. *)

Lemma sums2__cong34 : forall A B C D E F C' D', SumS A B C D E F -> SumS A B C' D' E F ->
  Cong C D C' D'.
Proof.
(* Goal: forall (A B C D E F C' D' : @Tpoint Tn) (_ : @SumS Tn A B C D E F) (_ : @SumS Tn A B C' D' E F), @Cong Tn C D C' D' *)
  intros A B C D E F C' D' HSumS HSumS'.
(* Goal: @Cong Tn C D C' D' *)
  apply sums2__cong12 with A B E F; apply sums_sym; trivial.
Qed.

(** Cong preserves SumS *)

Lemma cong3_sums__sums : forall A B C D E F A' B' C' D' E' F',
  Cong A B A' B' -> Cong C D C' D' -> Cong E F E' F' -> SumS A B C D E F ->
  SumS A' B' C' D' E' F'.
Proof.
(* Goal: forall (A B C D E F A' B' C' D' E' F' : @Tpoint Tn) (_ : @Cong Tn A B A' B') (_ : @Cong Tn C D C' D') (_ : @Cong Tn E F E' F') (_ : @SumS Tn A B C D E F), @SumS Tn A' B' C' D' E' F' *)
  intros A B C D E F A' B' C' D' E' F' HCong1 HCong2 HCong3 HSumS.
(* Goal: @SumS Tn A' B' C' D' E' F' *)
  destruct HSumS as [P [Q [R [HBet [HCong4 [HCong5 HCong6]]]]]].
(* Goal: @SumS Tn A' B' C' D' E' F' *)
  exists P, Q, R; repeat split; trivial; eapply cong_transitivity; eauto.
Qed.

(** The degenerate segments represent the additive identity *)

Lemma sums123312 : forall A B C, SumS A B C C A B.
Proof.
(* Goal: forall A B C : @Tpoint Tn, @SumS Tn A B C C A B *)
  intros A B C.
(* Goal: @SumS Tn A B C C A B *)
  exists A, B, B.
(* Goal: and (@Bet Tn A B B) (and (@Cong Tn A B A B) (and (@Cong Tn B B C C) (@Cong Tn A B A B))) *)
  repeat split; Between; Cong.
Qed.

Lemma sums__cong1245 : forall A B C D E, SumS A B C C D E -> Cong A B D E.
Proof.
(* Goal: forall (A B C D E : @Tpoint Tn) (_ : @SumS Tn A A B C D E), @Cong Tn B C D E *)
  intros A B C D E HSum.
(* Goal: @Cong Tn A B D E *)
  apply (sums2__cong56 A B C C); trivial.
(* Goal: @SumS Tn A B C C A B *)
  apply sums123312.
Qed.

Lemma sums__eq34 : forall A B C D, SumS A B C D A B -> C = D.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @SumS Tn A B C D C D), @eq (@Tpoint Tn) A B *)
  intros A B C D HSum.
(* Goal: @eq (@Tpoint Tn) C D *)
  apply cong_identity with C.
(* Goal: @Cong Tn C D C C *)
  apply sums2__cong34 with A B A B; trivial.
(* Goal: @SumS Tn A B C C A B *)
  apply sums123312.
Qed.

Lemma sums112323 : forall A B C, SumS A A B C B C.
Proof.
(* Goal: forall A B C : @Tpoint Tn, @SumS Tn A A B C B C *)
  intros; apply sums_sym, sums123312.
Qed.

Lemma sums__cong2345 : forall A B C D E, SumS A A B C D E -> Cong B C D E.
Proof.
(* Goal: forall (A B C D E : @Tpoint Tn) (_ : @SumS Tn A A B C D E), @Cong Tn B C D E *)
  intros A B C D E HSum.
(* Goal: @Cong Tn B C D E *)
  apply (sums2__cong56 A A B C); trivial.
(* Goal: @SumS Tn A A C D C D *)
  apply sums112323.
Qed.

Lemma sums__eq12 : forall A B C D, SumS A B C D C D -> A = B.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @SumS Tn A B C D C D), @eq (@Tpoint Tn) A B *)
  intros A B C D HSum.
(* Goal: @eq (@Tpoint Tn) A B *)
  apply cong_identity with A.
(* Goal: @Cong Tn A B A A *)
  apply sums2__cong12 with C D C D; trivial.
(* Goal: @SumS Tn A A C D C D *)
  apply sums112323.
Qed.

(** Some permutation properties *)

Lemma sums_left_comm : forall A B C D E F, SumS A B C D E F -> SumS B A C D E F.
Proof.
(* Goal: forall (A B C D E F : @Tpoint Tn) (_ : @SumS Tn A B C D E F), @Le Tn C D E F *)
  intros A B C D E F HSumS.
(* Goal: @SumS Tn A B C D F E *)
  apply (cong3_sums__sums A B C D E F); Cong.
Qed.

Lemma sums_middle_comm : forall A B C D E F, SumS A B C D E F -> SumS A B D C E F.
Proof.
(* Goal: forall (A B C D E F : @Tpoint Tn) (_ : @SumS Tn A B C D E F), @SumS Tn A B D C E F *)
  intros; apply sums_sym, sums_left_comm, sums_sym; trivial.
Qed.

Lemma sums_right_comm : forall A B C D E F, SumS A B C D E F -> SumS A B C D F E.
Proof.
(* Goal: forall (A B C D E F : @Tpoint Tn) (_ : @SumS Tn A B C D E F), @Le Tn C D E F *)
  intros A B C D E F HSumS.
(* Goal: @SumS Tn A B C D F E *)
  apply (cong3_sums__sums A B C D E F); Cong.
Qed.

Lemma sums_comm : forall A B C D E F, SumS A B C D E F -> SumS B A D C F E.
Proof.
(* Goal: forall (A B C D E F : @Tpoint Tn) (_ : @SumS Tn A B C D E F), @SumS Tn B A D C F E *)
  intros; apply sums_left_comm, sums_middle_comm, sums_right_comm; trivial.
Qed.

(** Basic case of sum *)

Lemma bet__sums : forall A B C, Bet A B C -> SumS A B B C A C.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Bet Tn A B C), @SumS Tn A B B C A C *)
  intros A B C HBet.
(* Goal: and (@Bet Tn A B R) (and (@Cong Tn A B A B) (and (@Cong Tn B R C D) (@Cong Tn A R A R))) *)
  exists A, B, C; repeat split; Cong.
Qed.


Lemma sums_assoc_1 : forall A B C D E F G H I J K L,
  SumS A B C D G H -> SumS C D E F I J -> SumS G H E F K L ->
  SumS A B I J K L.
Proof.
(* Goal: forall (A B C D E F G H I J K L : @Tpoint Tn) (_ : @SumS Tn A B C D G H) (_ : @SumS Tn C D E F I J) (_ : @SumS Tn A B I J K L), @SumS Tn G H E F K L *)
  intros A B C D E F G H I J K L HSumS1 HSumS2 HSumS3.
(* Goal: @SumS Tn A B I J K L *)
  destruct HSumS1 as [P [Q [R [HBet [HCong1 [HCong2 HCong3]]]]]].
(* Goal: @SumS Tn A B I J K L *)
  destruct (segment_construction P R E F) as [S [HS1 HS2]].
(* Goal: @SumS Tn A B I J K L *)
  exists P, Q, S; repeat split; trivial.
  - apply between_exchange4 with R; trivial.
  - apply (sums2__cong56 C D E F); trivial.
(* Goal: and (@Bet Tn A B R) (and (@Cong Tn A B A B) (and (@Cong Tn B R C D) (@Cong Tn A R A R))) *)
    exists Q, R, S; repeat split; Cong.
(* Goal: @Bet Tn Q R S *)
    apply between_exchange3 with P; trivial.
  - apply (sums2__cong56 G H E F); trivial.
(* Goal: and (@Bet Tn A B R) (and (@Cong Tn A B A B) (and (@Cong Tn B R C D) (@Cong Tn A R A R))) *)
    exists P, R, S; repeat split; Cong.
Qed.

Lemma sums_assoc_2 : forall A B C D E F G H I J K L,
  SumS A B C D G H -> SumS C D E F I J -> SumS A B I J K L ->
  SumS G H E F K L.
Proof.
(* Goal: forall (A B C D E F G H I J K L : @Tpoint Tn) (_ : @SumS Tn A B C D G H) (_ : @SumS Tn C D E F I J) (_ : @SumS Tn A B I J K L), @SumS Tn G H E F K L *)
  intros A B C D E F G H I J K L HSumS1 HSumS2 HSumS3.
(* Goal: @SumS Tn G H E F K L *)
  apply sums_sym, sums_assoc_1 with C D A B I J; apply sums_sym; trivial.
Qed.

(** Associativity of the sum. *)

Lemma sums_assoc : forall A B C D E F G H I J K L,
  SumS A B C D G H -> SumS C D E F I J ->
  (SumS G H E F K L <-> SumS A B I J K L).
Proof.
(* Goal: forall (A B C D E F G H I J K L : @Tpoint Tn) (_ : @SumS Tn A B C D G H) (_ : @SumS Tn C D E F I J), iff (@SumS Tn G H E F K L) (@SumS Tn A B I J K L) *)
  intros A B C D E F G H I J K L HSumS1 HSumS2.
(* Goal: iff (@SumS Tn G H E F K L) (@SumS Tn A B I J K L) *)
  split; intro HSumS3.
  - apply sums_assoc_1 with C D E F G H; trivial.
  - apply sums_assoc_2 with A B C D I J; trivial.
Qed.

(** AB <= AB + CD *)

Lemma sums__le1256 : forall A B C D E F, SumS A B C D E F -> Le A B E F.
Proof.
(* Goal: forall (A B C D E F : @Tpoint Tn) (_ : @SumS Tn A B C D E F), @Le Tn C D E F *)
  intros A B C D E F HSumS.
(* Goal: @Le Tn E F E' F' *)
  destruct HSumS as [P [Q [R [HBet [HCong1 [HCong2 HCong3]]]]]].
(* Goal: @Le Tn A B E F *)
  apply (l5_6 P Q P R); trivial.
(* Goal: @Le Tn P Q P R *)
  exists Q; Cong.
Qed.

(** CD <= AB + CD *)

Lemma sums__le3456 : forall A B C D E F, SumS A B C D E F -> Le C D E F.
Proof.
(* Goal: forall (A B C D E F : @Tpoint Tn) (_ : @SumS Tn A B C D E F), @Le Tn C D E F *)
  intros A B C D E F HSumS.
(* Goal: @Le Tn C D E F *)
  apply sums__le1256 with A B, sums_sym; trivial.
Qed.

(** If the sum of two segments is degenerate, then the segments are degenerate *)

Lemma eq_sums__eq : forall A B C D E, SumS A B C D E E -> A = B /\ C = D.
Proof.
(* Goal: forall (A B C D E : @Tpoint Tn) (_ : @SumS Tn A B C D E E), and (@eq (@Tpoint Tn) A B) (@eq (@Tpoint Tn) C D) *)
  intros A B C D E HSumS.
(* Goal: and (@eq (@Tpoint Tn) A B) (@eq (@Tpoint Tn) C D) *)
  split; apply le_zero with E; [apply sums__le1256 with C D|apply (sums__le3456 A B)]; assumption.
Qed.

Lemma sums_diff_1 : forall A B C D E F, A <> B -> SumS A B C D E F -> E <> F.
Proof.
(* Goal: forall (A B C D E F : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) C D)) (_ : @SumS Tn A B C D E F), not (@eq (@Tpoint Tn) E F) *)
  intros A B C D E F Hdiff HSumS Heq.
(* Goal: False *)
  subst F.
(* Goal: False *)
  apply Hdiff.
(* Goal: @eq (@Tpoint Tn) C D *)
  destruct (eq_sums__eq A B C D E HSumS); assumption.
Qed.

Lemma sums_diff_2 : forall A B C D E F, C <> D -> SumS A B C D E F -> E <> F.
Proof.
(* Goal: forall (A B C D E F : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) C D)) (_ : @SumS Tn A B C D E F), not (@eq (@Tpoint Tn) E F) *)
  intros A B C D E F Hdiff HSumS Heq.
(* Goal: False *)
  subst F.
(* Goal: False *)
  apply Hdiff.
(* Goal: @eq (@Tpoint Tn) C D *)
  destruct (eq_sums__eq A B C D E HSumS); assumption.
Qed.

(** SumS preserves Le *)

Lemma le2_sums2__le : forall A B C D E F A' B' C' D' E' F',
  Le A B A' B' -> Le C D C' D' -> SumS A B C D E F -> SumS A' B' C' D' E' F' ->
  Le E F E' F'.
Proof.
(* Goal: forall (A B C D E F A' B' C' D' E' F' : @Tpoint Tn) (_ : @Le Tn A B A' B') (_ : @Le Tn C D C' D') (_ : @SumS Tn A B C D E F) (_ : @SumS Tn A' B' C' D' E' F'), @Le Tn E F E' F' *)
  intros A B C D E F A' B' C' D' E' F' HLe1 HLe2 HSumS HSumS'.
(* Goal: @Le Tn E F E' F' *)
  destruct HSumS as [P [Q [R [HBet [HCong1 [HCong2 HCong3]]]]]].
(* Goal: @Le Tn E F E' F' *)
  destruct HSumS' as [P' [Q' [R' [HBet' [HCong1' [HCong2' HCong3']]]]]].
(* Goal: @Le Tn E F E' F' *)
  apply (l5_6 P R P' R'); trivial.
(* Goal: @Le Tn P R P' R' *)
  apply bet2_le2__le1346 with Q Q'; trivial.
(* Goal: @Le Tn P Q P' Q' *)
(* Goal: @Le Tn Q R Q' R' *)
  apply (l5_6 A B A' B'); Cong.
(* Goal: @Le Tn Q R Q' R' *)
  apply (l5_6 C D C' D'); Cong.
Qed.

(** If AB <= A'B', CD <= C'D' and AB + CD = A'B' + C'D', then AB = A'B' and CD = C'D' *)

Lemma le2_sums2__cong12 : forall A B C D E F A' B' C' D',
  Le A B A' B' -> Le C D C' D' -> SumS A B C D E F -> SumS A' B' C' D' E F ->
  Cong A B A' B'.
Proof.
(* Goal: forall (A B C D E F A' B' C' D' : @Tpoint Tn) (_ : @Le Tn A B A' B') (_ : @Le Tn C D C' D') (_ : @SumS Tn A B C D E F) (_ : @SumS Tn A' B' C' D' E F), @Cong Tn C D C' D' *)
  intros A B C D E F A' B' C' D' HLe1 HLe2 HSum HSum'.
(* Goal: @Cong Tn A B A' B' *)
  apply sums2__cong12 with C D E F; trivial.
(* Goal: @SumS Tn A' B' C D E F *)
  destruct (ex_sums A' B' C D) as [E' [F' HSum1]].
(* Goal: @SumS Tn A' B' C D E F *)
  apply (cong3_sums__sums A' B' C D E' F'); Cong.
(* Goal: @Cong Tn E' F' E F *)
  apply le_anti_symmetry.
(* Goal: @Le Tn E' F' E F *)
(* Goal: @Le Tn E F E' F' *)
    apply le2_sums2__le with A' B' C D A' B' C' D'; Le.
(* Goal: @Le Tn E F E' F' *)
    apply le2_sums2__le with A B C D A' B' C D; Le.
Qed.

Lemma le2_sums2__cong34 : forall A B C D E F A' B' C' D',
  Le A B A' B' -> Le C D C' D' -> SumS A B C D E F -> SumS A' B' C' D' E F ->
  Cong C D C' D'.
Proof.
(* Goal: forall (A B C D E F A' B' C' D' : @Tpoint Tn) (_ : @Le Tn A B A' B') (_ : @Le Tn C D C' D') (_ : @SumS Tn A B C D E F) (_ : @SumS Tn A' B' C' D' E F), @Cong Tn C D C' D' *)
  intros A B C D E F A' B' C' D' HLe1 HLe2 HSum HSum'.
(* Goal: @Cong Tn C D C' D' *)
  apply le2_sums2__cong12 with A B E F A' B'; try (apply sums_sym); trivial.
Qed.

(** If AB < A'B' and CD <= C'D', then AB + CD < A'B' + C'D' *)

Lemma le_lt12_sums2__lt : forall A B C D E F A' B' C' D' E' F',
  Lt A B A' B' -> Le C D C' D' -> SumS A B C D E F -> SumS A' B' C' D' E' F' ->
  Lt E F E' F'.
Proof.
(* Goal: forall (A B C D E F A' B' C' D' E' F' : @Tpoint Tn) (_ : @Lt Tn C' D' C D) (_ : @Le Tn E F E' F') (_ : @SumS Tn A B C D E F) (_ : @SumS Tn A' B' C' D' E' F'), @Lt Tn A B A' B' *)
  intros A B C D E F A' B' C' D' E' F' HLt HLe HSum HSum'.
(* Goal: @Lt Tn E F E' F' *)
  split.
(* Goal: @Le Tn E F E' F' *)
(* Goal: not (@Cong Tn E F E' F') *)
    apply le2_sums2__le with A B C D A' B' C' D'; Le.
(* Goal: not (@Cong Tn E F E' F') *)
  intro HCong.
(* Goal: False *)
  destruct HLt as [HLe1 HNCong].
(* Goal: False *)
  apply HNCong.
(* Goal: @Cong Tn A B A' B' *)
  apply le2_sums2__cong12 with C D E F C' D'; trivial.
(* Goal: @SumS Tn A' B' C' D' E F *)
  apply (cong3_sums__sums A' B' C' D' E' F'); Cong.
Qed.

Lemma le_lt34_sums2__lt : forall A B C D E F A' B' C' D' E' F',
  Le A B A' B' -> Lt C D C' D' -> SumS A B C D E F -> SumS A' B' C' D' E' F' ->
  Lt E F E' F'.
Proof.
(* Goal: forall (A B C D E F A' B' C' D' E' F' : @Tpoint Tn) (_ : @Lt Tn A' B' A B) (_ : @Lt Tn E F E' F') (_ : @SumS Tn A B C D E F) (_ : @SumS Tn A' B' C' D' E' F'), @Lt Tn C D C' D' *)
  intros A B C D E F A' B' C' D' E' F' HLe HLt HSum HSum'.
(* Goal: @Lt Tn E F E' F' *)
  apply le_lt12_sums2__lt with C D A B C' D' A' B'; try (apply sums_sym); trivial.
Qed.

Lemma lt2_sums2__lt : forall A B C D E F A' B' C' D' E' F',
  Lt A B A' B' -> Lt C D C' D' -> SumS A B C D E F -> SumS A' B' C' D' E' F' ->
  Lt E F E' F'.
Proof.
(* Goal: forall (A B C D E F A' B' C' D' E' F' : @Tpoint Tn) (_ : @Lt Tn C' D' C D) (_ : @Lt Tn E F E' F') (_ : @SumS Tn A B C D E F) (_ : @SumS Tn A' B' C' D' E' F'), @Lt Tn A B A' B' *)
  intros A B C D E F A' B' C' D' E' F' HLt1 HLt2 HSum HSum'.
(* Goal: @Lt Tn E F E' F' *)
  apply le_lt12_sums2__lt with A B C D A' B' C' D'; Le.
Qed.

(** If CD >= C'D' and AB + CD <= A'B' + C'D', then AB <= A'B' *)

Lemma le2_sums2__le12 : forall A B C D E F A' B' C' D' E' F',
  Le C' D' C D -> Le E F E' F' -> SumS A B C D E F -> SumS A' B' C' D' E' F' ->
  Le A B A' B'.
Proof.
(* Goal: forall (A B C D E F A' B' C' D' E' F' : @Tpoint Tn) (_ : @Lt Tn A' B' A B) (_ : @Le Tn E F E' F') (_ : @SumS Tn A B C D E F) (_ : @SumS Tn A' B' C' D' E' F'), @Lt Tn C D C' D' *)
  intros A B C D E F A' B' C' D' E' F' HLe1 HLe2 HSum HSum'.
(* Goal: @Le Tn A B A' B' *)
  apply nlt__le; intro HLt.
(* Goal: False *)
  apply le__nlt in HLe2; apply HLe2.
(* Goal: @Lt Tn E' F' E F *)
  apply le_lt12_sums2__lt with A' B' C' D' A B C D; trivial.
Qed.

Lemma le2_sums2__le34 : forall A B C D E F A' B' C' D' E' F',
  Le A' B' A B -> Le E F E' F' -> SumS A B C D E F -> SumS A' B' C' D' E' F' ->
  Le C D C' D'.
Proof.
(* Goal: forall (A B C D E F A' B' C' D' E' F' : @Tpoint Tn) (_ : @Lt Tn A' B' A B) (_ : @Le Tn E F E' F') (_ : @SumS Tn A B C D E F) (_ : @SumS Tn A' B' C' D' E' F'), @Lt Tn C D C' D' *)
  intros A B C D E F A' B' C' D' E' F' HLe1 HLe2 HSum HSum'.
(* Goal: @Le Tn C D C' D' *)
  apply le2_sums2__le12 with A B E F A' B' E' F'; try (apply sums_sym); trivial.
Qed.

(** If CD > C'D' and AB + CD <= A'B' + C'D', then AB < A'B' *)

Lemma le_lt34_sums2__lt12 : forall A B C D E F A' B' C' D' E' F',
  Lt C' D' C D -> Le E F E' F' -> SumS A B C D E F -> SumS A' B' C' D' E' F' ->
  Lt A B A' B'.
Proof.
(* Goal: forall (A B C D E F A' B' C' D' E' F' : @Tpoint Tn) (_ : @Lt Tn C' D' C D) (_ : @Le Tn E F E' F') (_ : @SumS Tn A B C D E F) (_ : @SumS Tn A' B' C' D' E' F'), @Lt Tn A B A' B' *)
  intros A B C D E F A' B' C' D' E' F' HLt HLe HSum HSum'.
(* Goal: @Lt Tn A B A' B' *)
  apply nle__lt; intro HLe1.
(* Goal: False *)
  apply le__nlt in HLe; apply HLe.
(* Goal: @Lt Tn E' F' E F *)
  apply le_lt34_sums2__lt with A' B' C' D' A B C D; trivial.
Qed.

Lemma le_lt12_sums2__lt34 : forall A B C D E F A' B' C' D' E' F',
  Lt A' B' A B -> Le E F E' F' -> SumS A B C D E F -> SumS A' B' C' D' E' F' ->
  Lt C D C' D'.
Proof.
(* Goal: forall (A B C D E F A' B' C' D' E' F' : @Tpoint Tn) (_ : @Lt Tn A' B' A B) (_ : @Le Tn E F E' F') (_ : @SumS Tn A B C D E F) (_ : @SumS Tn A' B' C' D' E' F'), @Lt Tn C D C' D' *)
  intros A B C D E F A' B' C' D' E' F' HLe1 HLe2 HSum HSum'.
(* Goal: @Lt Tn C D C' D' *)
  apply le_lt34_sums2__lt12 with A B E F A' B' E' F'; try (apply sums_sym); trivial.
Qed.

(** If CD >= C'D' and AB + CD < A'B' + C'D', then AB < A'B' *)

Lemma le_lt56_sums2__lt12 : forall A B C D E F A' B' C' D' E' F',
  Le C' D' C D -> Lt E F E' F' -> SumS A B C D E F -> SumS A' B' C' D' E' F' ->
  Lt A B A' B'.
Proof.
(* Goal: forall (A B C D E F A' B' C' D' E' F' : @Tpoint Tn) (_ : @Lt Tn A' B' A B) (_ : @Lt Tn E F E' F') (_ : @SumS Tn A B C D E F) (_ : @SumS Tn A' B' C' D' E' F'), @Lt Tn C D C' D' *)
  intros A B C D E F A' B' C' D' E' F' HLe HLt HSum HSum'.
(* Goal: @Lt Tn A B A' B' *)
  apply nle__lt; intro HLe1.
(* Goal: False *)
  apply lt__nle in HLt; apply HLt.
(* Goal: @Le Tn E' F' E F *)
  apply le2_sums2__le with A' B' C' D' A B C D; trivial.
Qed.

Lemma le_lt56_sums2__lt34 : forall A B C D E F A' B' C' D' E' F',
  Le A' B' A B -> Lt E F E' F' -> SumS A B C D E F -> SumS A' B' C' D' E' F' ->
  Lt C D C' D'.
Proof.
(* Goal: forall (A B C D E F A' B' C' D' E' F' : @Tpoint Tn) (_ : @Lt Tn A' B' A B) (_ : @Lt Tn E F E' F') (_ : @SumS Tn A B C D E F) (_ : @SumS Tn A' B' C' D' E' F'), @Lt Tn C D C' D' *)
  intros A B C D E F A' B' C' D' E' F' HLe HLt HSum HSum'.
(* Goal: @Lt Tn C D C' D' *)
  apply le_lt56_sums2__lt12 with A B E F A' B' E' F'; try (apply sums_sym); trivial.
Qed.

Lemma lt2_sums2__lt12 : forall A B C D E F A' B' C' D' E' F',
  Lt C' D' C D -> Lt E F E' F' -> SumS A B C D E F -> SumS A' B' C' D' E' F' ->
  Lt A B A' B'.
Proof.
(* Goal: forall (A B C D E F A' B' C' D' E' F' : @Tpoint Tn) (_ : @Lt Tn C' D' C D) (_ : @Lt Tn E F E' F') (_ : @SumS Tn A B C D E F) (_ : @SumS Tn A' B' C' D' E' F'), @Lt Tn A B A' B' *)
  intros A B C D E F A' B' C' D' E' F' HLt1 HLt2 HSum HSum'.
(* Goal: @Lt Tn A B A' B' *)
  apply le_lt56_sums2__lt12 with C D E F C' D' E' F'; Le.
Qed.

Lemma lt2_sums2__lt34 : forall A B C D E F A' B' C' D' E' F',
  Lt A' B' A B -> Lt E F E' F' -> SumS A B C D E F -> SumS A' B' C' D' E' F' ->
  Lt C D C' D'.
Proof.
(* Goal: forall (A B C D E F A' B' C' D' E' F' : @Tpoint Tn) (_ : @Lt Tn A' B' A B) (_ : @Lt Tn E F E' F') (_ : @SumS Tn A B C D E F) (_ : @SumS Tn A' B' C' D' E' F'), @Lt Tn C D C' D' *)
  intros A B C D E F A' B' C' D' E' F' HLe HLt HSum HSum'.
(* Goal: @Lt Tn C D C' D' *)
  apply le_lt56_sums2__lt34 with A B E F A' B' E' F'; Le.
Qed.

End Sums.

Hint Resolve sums__le1256 sums__le3456 : le.

Hint Resolve sums_sym sums_left_comm sums_middle_comm sums_right_comm
             sums_comm sums112323 sums123312 bet__sums : sums.

Ltac Sums := auto with sums.