Rsigma.v

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Require Import Rbase.
Require Import Rfunctions.
Require Import Rseries.
Require Import PartSum.
Require Import Omega.
Local Open Scope R_scope.

Set Implicit Arguments.

Section Sigma.

  Variable f : nat -> R.

  Definition sigma (low high:nat) : R :=
    sum_f_R0 (fun k:nat => f (low + k)) (high - low).

  Theorem sigma_split :
    forall low high k:nat,
      (low <= k)%nat ->
      (k < high)%nat -> sigma low high = sigma low k + sigma (S k) high.f:nat -> R
forall low high k : nat,
(low <= k)%nat ->
(k < high)%nat ->
sigma low high = sigma low k + sigma (S k) high
  Proof.f:nat -> R
forall low high k : nat,
(low <= k)%nat ->
(k < high)%nat ->
sigma low high = sigma low k + sigma (S k) high
    intros; induction  k as [| k Hreck].f:nat -> R
low, high:nat
H:(low <= 0)%nat
H0:(0 < high)%nat
sigma low high = sigma low 0 + sigma 1 high
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
sigma low high =
sigma low (S k) + sigma (S (S k)) high
    cut (low = 0%nat).f:nat -> R
low, high:nat
H:(low <= 0)%nat
H0:(0 < high)%nat
low = 0%nat ->
sigma low high = sigma low 0 + sigma 1 high
f:nat -> R
low, high:nat
H:(low <= 0)%nat
H0:(0 < high)%nat
low = 0%nat
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
sigma low high =
sigma low (S k) + sigma (S (S k)) high
    intro; rewrite H1; unfold sigma; rewrite <- minus_n_n;
      rewrite <- minus_n_O; simpl; replace (high - 1)%nat with (pred high).f:nat -> R
low, high:nat
H:(low <= 0)%nat
H0:(0 < high)%nat
H1:low = 0%nat
sum_f_R0 (fun k : nat => f k) high =
f 0 +
sum_f_R0 (fun k : nat => f (S k)) (Init.Nat.pred high)
f:nat -> R
low, high:nat
H:(low <= 0)%nat
H0:(0 < high)%nat
H1:low = 0%nat
Init.Nat.pred high = (high - 1)%nat
f:nat -> R
low, high:nat
H:(low <= 0)%nat
H0:(0 < high)%nat
low = 0%nat
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
sigma low high =
sigma low (S k) + sigma (S (S k)) high
    apply (decomp_sum (fun k:nat => f k)).f:nat -> R
low, high:nat
H:(low <= 0)%nat
H0:(0 < high)%nat
H1:low = 0%nat
(0 < high)%nat
f:nat -> R
low, high:nat
H:(low <= 0)%nat
H0:(0 < high)%nat
H1:low = 0%nat
Init.Nat.pred high = (high - 1)%nat
f:nat -> R
low, high:nat
H:(low <= 0)%nat
H0:(0 < high)%nat
low = 0%nat
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
sigma low high =
sigma low (S k) + sigma (S (S k)) high
    assumption.f:nat -> R
low, high:nat
H:(low <= 0)%nat
H0:(0 < high)%nat
H1:low = 0%nat
Init.Nat.pred high = (high - 1)%nat
f:nat -> R
low, high:nat
H:(low <= 0)%nat
H0:(0 < high)%nat
low = 0%nat
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
sigma low high =
sigma low (S k) + sigma (S (S k)) high
    apply pred_of_minus.f:nat -> R
low, high:nat
H:(low <= 0)%nat
H0:(0 < high)%nat
low = 0%nat
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
sigma low high =
sigma low (S k) + sigma (S (S k)) high
    inversion H; reflexivity.f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
sigma low high =
sigma low (S k) + sigma (S (S k)) high
    cut ((low <= k)%nat \/ low = S k).f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
(low <= k)%nat \/ low = S k ->
sigma low high =
sigma low (S k) + sigma (S (S k)) high
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
(low <= k)%nat \/ low = S k
    intro; elim H1; intro.f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:(low <= k)%nat
sigma low high =
sigma low (S k) + sigma (S (S k)) high
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:low = S k
sigma low high =
sigma low (S k) + sigma (S (S k)) high
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
(low <= k)%nat \/ low = S k
    replace (sigma low (S k)) with (sigma low k + f (S k)).f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:(low <= k)%nat
sigma low high =
sigma low k + f (S k) + sigma (S (S k)) high
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:(low <= k)%nat
sigma low k + f (S k) = sigma low (S k)
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:low = S k
sigma low high =
sigma low (S k) + sigma (S (S k)) high
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
(low <= k)%nat \/ low = S k
    rewrite Rplus_assoc;
      replace (f (S k) + sigma (S (S k)) high) with (sigma (S k) high).f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:(low <= k)%nat
sigma low high = sigma low k + sigma (S k) high
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:(low <= k)%nat
sigma (S k) high = f (S k) + sigma (S (S k)) high
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:(low <= k)%nat
sigma low k + f (S k) = sigma low (S k)
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:low = S k
sigma low high =
sigma low (S k) + sigma (S (S k)) high
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
(low <= k)%nat \/ low = S k
    apply Hreck.f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:(low <= k)%nat
(low <= k)%nat
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:(low <= k)%nat
(k < high)%nat
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:(low <= k)%nat
sigma (S k) high = f (S k) + sigma (S (S k)) high
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:(low <= k)%nat
sigma low k + f (S k) = sigma low (S k)
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:low = S k
sigma low high =
sigma low (S k) + sigma (S (S k)) high
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
(low <= k)%nat \/ low = S k
    assumption.f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:(low <= k)%nat
(k < high)%nat
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:(low <= k)%nat
sigma (S k) high = f (S k) + sigma (S (S k)) high
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:(low <= k)%nat
sigma low k + f (S k) = sigma low (S k)
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:low = S k
sigma low high =
sigma low (S k) + sigma (S (S k)) high
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
(low <= k)%nat \/ low = S k
    apply lt_trans with (S k); [ apply lt_n_Sn | assumption ].f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:(low <= k)%nat
sigma (S k) high = f (S k) + sigma (S (S k)) high
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:(low <= k)%nat
sigma low k + f (S k) = sigma low (S k)
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:low = S k
sigma low high =
sigma low (S k) + sigma (S (S k)) high
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
(low <= k)%nat \/ low = S k
    unfold sigma; replace (high - S (S k))%nat with (pred (high - S k)).f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:(low <= k)%nat
sum_f_R0 (fun k0 : nat => f (S k + k0)) (high - S k) =
f (S k) +
sum_f_R0 (fun k0 : nat => f (S (S k) + k0))
  (Init.Nat.pred (high - S k))
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:(low <= k)%nat
Init.Nat.pred (high - S k) = (high - S (S k))%nat
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:(low <= k)%nat
sigma low k + f (S k) = sigma low (S k)
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:low = S k
sigma low high =
sigma low (S k) + sigma (S (S k)) high
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
(low <= k)%nat \/ low = S k
    pattern (S k) at 3; replace (S k) with (S k + 0)%nat;
      [ idtac | ring ].f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:(low <= k)%nat
sum_f_R0 (fun k0 : nat => f (S k + k0)) (high - S k) =
f (S k + 0) +
sum_f_R0 (fun k0 : nat => f (S (S k) + k0))
  (Init.Nat.pred (high - S k))
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:(low <= k)%nat
Init.Nat.pred (high - S k) = (high - S (S k))%nat
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:(low <= k)%nat
sigma low k + f (S k) = sigma low (S k)
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:low = S k
sigma low high =
sigma low (S k) + sigma (S (S k)) high
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
(low <= k)%nat \/ low = S k
    replace (sum_f_R0 (fun k0:nat => f (S (S k) + k0)) (pred (high - S k))) with
    (sum_f_R0 (fun k0:nat => f (S k + S k0)) (pred (high - S k))).f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:(low <= k)%nat
sum_f_R0 (fun k0 : nat => f (S k + k0)) (high - S k) =
f (S k + 0) +
sum_f_R0 (fun k0 : nat => f (S k + S k0))
  (Init.Nat.pred (high - S k))
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:(low <= k)%nat
sum_f_R0 (fun k0 : nat => f (S k + S k0))
  (Init.Nat.pred (high - S k)) =
sum_f_R0 (fun k0 : nat => f (S (S k) + k0))
  (Init.Nat.pred (high - S k))
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:(low <= k)%nat
Init.Nat.pred (high - S k) = (high - S (S k))%nat
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:(low <= k)%nat
sigma low k + f (S k) = sigma low (S k)
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:low = S k
sigma low high =
sigma low (S k) + sigma (S (S k)) high
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
(low <= k)%nat \/ low = S k
    apply (decomp_sum (fun i:nat => f (S k + i))).f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:(low <= k)%nat
(0 < high - S k)%nat
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:(low <= k)%nat
sum_f_R0 (fun k0 : nat => f (S k + S k0))
  (Init.Nat.pred (high - S k)) =
sum_f_R0 (fun k0 : nat => f (S (S k) + k0))
  (Init.Nat.pred (high - S k))
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:(low <= k)%nat
Init.Nat.pred (high - S k) = (high - S (S k))%nat
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:(low <= k)%nat
sigma low k + f (S k) = sigma low (S k)
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:low = S k
sigma low high =
sigma low (S k) + sigma (S (S k)) high
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
(low <= k)%nat \/ low = S k
    apply lt_minus_O_lt; assumption.f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:(low <= k)%nat
sum_f_R0 (fun k0 : nat => f (S k + S k0))
  (Init.Nat.pred (high - S k)) =
sum_f_R0 (fun k0 : nat => f (S (S k) + k0))
  (Init.Nat.pred (high - S k))
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:(low <= k)%nat
Init.Nat.pred (high - S k) = (high - S (S k))%nat
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:(low <= k)%nat
sigma low k + f (S k) = sigma low (S k)
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:low = S k
sigma low high =
sigma low (S k) + sigma (S (S k)) high
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
(low <= k)%nat \/ low = S k
    apply sum_eq; intros; replace (S k + S i)%nat with (S (S k) + i)%nat.f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:(low <= k)%nat
i:nat
H3:(i <= Init.Nat.pred (high - S k))%nat
f (S (S k) + i) = f (S (S k) + i)
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:(low <= k)%nat
i:nat
H3:(i <= Init.Nat.pred (high - S k))%nat
(S (S k) + i)%nat = (S k + S i)%nat
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:(low <= k)%nat
Init.Nat.pred (high - S k) = (high - S (S k))%nat
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:(low <= k)%nat
sigma low k + f (S k) = sigma low (S k)
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:low = S k
sigma low high =
sigma low (S k) + sigma (S (S k)) high
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
(low <= k)%nat \/ low = S k
    reflexivity.f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:(low <= k)%nat
i:nat
H3:(i <= Init.Nat.pred (high - S k))%nat
(S (S k) + i)%nat = (S k + S i)%nat
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:(low <= k)%nat
Init.Nat.pred (high - S k) = (high - S (S k))%nat
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:(low <= k)%nat
sigma low k + f (S k) = sigma low (S k)
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:low = S k
sigma low high =
sigma low (S k) + sigma (S (S k)) high
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
(low <= k)%nat \/ low = S k
    ring.f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:(low <= k)%nat
Init.Nat.pred (high - S k) = (high - S (S k))%nat
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:(low <= k)%nat
sigma low k + f (S k) = sigma low (S k)
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:low = S k
sigma low high =
sigma low (S k) + sigma (S (S k)) high
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
(low <= k)%nat \/ low = S k
    replace (high - S (S k))%nat with (high - S k - 1)%nat.f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:(low <= k)%nat
Init.Nat.pred (high - S k) = (high - S k - 1)%nat
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:(low <= k)%nat
(high - S k - 1)%nat = (high - S (S k))%nat
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:(low <= k)%nat
sigma low k + f (S k) = sigma low (S k)
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:low = S k
sigma low high =
sigma low (S k) + sigma (S (S k)) high
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
(low <= k)%nat \/ low = S k
    apply pred_of_minus.f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:(low <= k)%nat
(high - S k - 1)%nat = (high - S (S k))%nat
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:(low <= k)%nat
sigma low k + f (S k) = sigma low (S k)
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:low = S k
sigma low high =
sigma low (S k) + sigma (S (S k)) high
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
(low <= k)%nat \/ low = S k
    omega.f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:(low <= k)%nat
sigma low k + f (S k) = sigma low (S k)
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:low = S k
sigma low high =
sigma low (S k) + sigma (S (S k)) high
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
(low <= k)%nat \/ low = S k
    unfold sigma; replace (S k - low)%nat with (S (k - low)).f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:(low <= k)%nat
sum_f_R0 (fun k0 : nat => f (low + k0)) (k - low) +
f (S k) =
sum_f_R0 (fun k0 : nat => f (low + k0)) (S (k - low))
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:(low <= k)%nat
S (k - low) = (S k - low)%nat
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:low = S k
sigma low high =
sigma low (S k) + sigma (S (S k)) high
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
(low <= k)%nat \/ low = S k
    pattern (S k) at 1; replace (S k) with (low + S (k - low))%nat.f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:(low <= k)%nat
sum_f_R0 (fun k0 : nat => f (low + k0)) (k - low) +
f (low + S (k - low)) =
sum_f_R0 (fun k0 : nat => f (low + k0)) (S (k - low))
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:(low <= k)%nat
(low + S (k - low))%nat = S k
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:(low <= k)%nat
S (k - low) = (S k - low)%nat
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:low = S k
sigma low high =
sigma low (S k) + sigma (S (S k)) high
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
(low <= k)%nat \/ low = S k
    symmetry ; apply (tech5 (fun i:nat => f (low + i))).f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:(low <= k)%nat
(low + S (k - low))%nat = S k
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:(low <= k)%nat
S (k - low) = (S k - low)%nat
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:low = S k
sigma low high =
sigma low (S k) + sigma (S (S k)) high
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
(low <= k)%nat \/ low = S k
    omega.f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:(low <= k)%nat
S (k - low) = (S k - low)%nat
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:low = S k
sigma low high =
sigma low (S k) + sigma (S (S k)) high
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
(low <= k)%nat \/ low = S k
    omega.f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:low = S k
sigma low high =
sigma low (S k) + sigma (S (S k)) high
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
(low <= k)%nat \/ low = S k
    rewrite <- H2; unfold sigma; rewrite <- minus_n_n; simpl;
      replace (high - S low)%nat with (pred (high - low)).f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:low = S k
sum_f_R0 (fun k0 : nat => f (low + k0)) (high - low) =
f (low + 0) +
sum_f_R0 (fun k0 : nat => f (S (low + k0)))
  (Init.Nat.pred (high - low))
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:low = S k
Init.Nat.pred (high - low) = (high - S low)%nat
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
(low <= k)%nat \/ low = S k
    replace (sum_f_R0 (fun k0:nat => f (S (low + k0))) (pred (high - low))) with
    (sum_f_R0 (fun k0:nat => f (low + S k0)) (pred (high - low))).f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:low = S k
sum_f_R0 (fun k0 : nat => f (low + k0)) (high - low) =
f (low + 0) +
sum_f_R0 (fun k0 : nat => f (low + S k0))
  (Init.Nat.pred (high - low))
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:low = S k
sum_f_R0 (fun k0 : nat => f (low + S k0))
  (Init.Nat.pred (high - low)) =
sum_f_R0 (fun k0 : nat => f (S (low + k0)))
  (Init.Nat.pred (high - low))
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:low = S k
Init.Nat.pred (high - low) = (high - S low)%nat
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
(low <= k)%nat \/ low = S k
    apply (decomp_sum (fun k0:nat => f (low + k0))).f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:low = S k
(0 < high - low)%nat
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:low = S k
sum_f_R0 (fun k0 : nat => f (low + S k0))
  (Init.Nat.pred (high - low)) =
sum_f_R0 (fun k0 : nat => f (S (low + k0)))
  (Init.Nat.pred (high - low))
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:low = S k
Init.Nat.pred (high - low) = (high - S low)%nat
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
(low <= k)%nat \/ low = S k
    apply lt_minus_O_lt.f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:low = S k
(low < high)%nat
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:low = S k
sum_f_R0 (fun k0 : nat => f (low + S k0))
  (Init.Nat.pred (high - low)) =
sum_f_R0 (fun k0 : nat => f (S (low + k0)))
  (Init.Nat.pred (high - low))
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:low = S k
Init.Nat.pred (high - low) = (high - S low)%nat
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
(low <= k)%nat \/ low = S k
    apply le_lt_trans with (S k); [ rewrite H2; apply le_n | assumption ].f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:low = S k
sum_f_R0 (fun k0 : nat => f (low + S k0))
  (Init.Nat.pred (high - low)) =
sum_f_R0 (fun k0 : nat => f (S (low + k0)))
  (Init.Nat.pred (high - low))
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:low = S k
Init.Nat.pred (high - low) = (high - S low)%nat
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
(low <= k)%nat \/ low = S k
    apply sum_eq; intros; replace (S (low + i)) with (low + S i)%nat.f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:low = S k
i:nat
H3:(i <= Init.Nat.pred (high - low))%nat
f (low + S i) = f (low + S i)
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:low = S k
i:nat
H3:(i <= Init.Nat.pred (high - low))%nat
(low + S i)%nat = S (low + i)
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:low = S k
Init.Nat.pred (high - low) = (high - S low)%nat
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
(low <= k)%nat \/ low = S k
    reflexivity.f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:low = S k
i:nat
H3:(i <= Init.Nat.pred (high - low))%nat
(low + S i)%nat = S (low + i)
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:low = S k
Init.Nat.pred (high - low) = (high - S low)%nat
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
(low <= k)%nat \/ low = S k
    ring.f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
H1:(low <= k)%nat \/ low = S k
H2:low = S k
Init.Nat.pred (high - low) = (high - S low)%nat
f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
(low <= k)%nat \/ low = S k
    omega.f:nat -> R
low, high, k:nat
H:(low <= S k)%nat
H0:(S k < high)%nat
Hreck:(low <= k)%nat ->
(k < high)%nat ->
sigma low high =
sigma low k + sigma (S k) high
(low <= k)%nat \/ low = S k
    inversion H; [ right; reflexivity | left; assumption ].
  Qed.

  Theorem sigma_diff :
    forall low high k:nat,
      (low <= k)%nat ->
      (k < high)%nat -> sigma low high - sigma low k = sigma (S k) high.f:nat -> R
forall low high k : nat,
(low <= k)%nat ->
(k < high)%nat ->
sigma low high - sigma low k = sigma (S k) high
  Proof.f:nat -> R
forall low high k : nat,
(low <= k)%nat ->
(k < high)%nat ->
sigma low high - sigma low k = sigma (S k) high
    intros low high k H1 H2; symmetry ; rewrite (sigma_split H1 H2); ring.
  Qed.

  Theorem sigma_diff_neg :
    forall low high k:nat,
      (low <= k)%nat ->
      (k < high)%nat -> sigma low k - sigma low high = - sigma (S k) high.f:nat -> R
forall low high k : nat,
(low <= k)%nat ->
(k < high)%nat ->
sigma low k - sigma low high = - sigma (S k) high
  Proof.f:nat -> R
forall low high k : nat,
(low <= k)%nat ->
(k < high)%nat ->
sigma low k - sigma low high = - sigma (S k) high
    intros low high k H1 H2; rewrite (sigma_split H1 H2); ring.
  Qed.

  Theorem sigma_first :
    forall low high:nat,
      (low < high)%nat -> sigma low high = f low + sigma (S low) high.f:nat -> R
forall low high : nat,
(low < high)%nat ->
sigma low high = f low + sigma (S low) high
  Proof.f:nat -> R
forall low high : nat,
(low < high)%nat ->
sigma low high = f low + sigma (S low) high
    intros low high H1; generalize (lt_le_S low high H1); intro H2;
      generalize (lt_le_weak low high H1); intro H3;
        replace (f low) with (sigma low low).f:nat -> R
low, high:nat
H1:(low < high)%nat
H2:(S low <= high)%nat
H3:(low <= high)%nat
sigma low high = sigma low low + sigma (S low) high
f:nat -> R
low, high:nat
H1:(low < high)%nat
H2:(S low <= high)%nat
H3:(low <= high)%nat
sigma low low = f low
    apply sigma_split.f:nat -> R
low, high:nat
H1:(low < high)%nat
H2:(S low <= high)%nat
H3:(low <= high)%nat
(low <= low)%nat
f:nat -> R
low, high:nat
H1:(low < high)%nat
H2:(S low <= high)%nat
H3:(low <= high)%nat
(low < high)%nat
f:nat -> R
low, high:nat
H1:(low < high)%nat
H2:(S low <= high)%nat
H3:(low <= high)%nat
sigma low low = f low
    apply le_n.f:nat -> R
low, high:nat
H1:(low < high)%nat
H2:(S low <= high)%nat
H3:(low <= high)%nat
(low < high)%nat
f:nat -> R
low, high:nat
H1:(low < high)%nat
H2:(S low <= high)%nat
H3:(low <= high)%nat
sigma low low = f low
    assumption.f:nat -> R
low, high:nat
H1:(low < high)%nat
H2:(S low <= high)%nat
H3:(low <= high)%nat
sigma low low = f low
    unfold sigma; rewrite <- minus_n_n.f:nat -> R
low, high:nat
H1:(low < high)%nat
H2:(S low <= high)%nat
H3:(low <= high)%nat
sum_f_R0 (fun k : nat => f (low + k)) 0 = f low
    simpl.f:nat -> R
low, high:nat
H1:(low < high)%nat
H2:(S low <= high)%nat
H3:(low <= high)%nat
f (low + 0) = f low
    replace (low + 0)%nat with low; [ reflexivity | ring ].
  Qed.

  Theorem sigma_last :
    forall low high:nat,
      (low < high)%nat -> sigma low high = f high + sigma low (pred high).f:nat -> R
forall low high : nat,
(low < high)%nat ->
sigma low high =
f high + sigma low (Init.Nat.pred high)
  Proof.f:nat -> R
forall low high : nat,
(low < high)%nat ->
sigma low high =
f high + sigma low (Init.Nat.pred high)
    intros low high H1; generalize (lt_le_S low high H1); intro H2;
      generalize (lt_le_weak low high H1); intro H3;
        replace (f high) with (sigma high high).f:nat -> R
low, high:nat
H1:(low < high)%nat
H2:(S low <= high)%nat
H3:(low <= high)%nat
sigma low high =
sigma high high + sigma low (Init.Nat.pred high)
f:nat -> R
low, high:nat
H1:(low < high)%nat
H2:(S low <= high)%nat
H3:(low <= high)%nat
sigma high high = f high
    rewrite Rplus_comm; cut (high = S (pred high)).f:nat -> R
low, high:nat
H1:(low < high)%nat
H2:(S low <= high)%nat
H3:(low <= high)%nat
high = S (Init.Nat.pred high) ->
sigma low high =
sigma low (Init.Nat.pred high) + sigma high high
f:nat -> R
low, high:nat
H1:(low < high)%nat
H2:(S low <= high)%nat
H3:(low <= high)%nat
high = S (Init.Nat.pred high)
f:nat -> R
low, high:nat
H1:(low < high)%nat
H2:(S low <= high)%nat
H3:(low <= high)%nat
sigma high high = f high
    intro; pattern high at 3; rewrite H.f:nat -> R
low, high:nat
H1:(low < high)%nat
H2:(S low <= high)%nat
H3:(low <= high)%nat
H:high = S (Init.Nat.pred high)
sigma low high =
sigma low (Init.Nat.pred high) +
sigma (S (Init.Nat.pred high)) high
f:nat -> R
low, high:nat
H1:(low < high)%nat
H2:(S low <= high)%nat
H3:(low <= high)%nat
high = S (Init.Nat.pred high)
f:nat -> R
low, high:nat
H1:(low < high)%nat
H2:(S low <= high)%nat
H3:(low <= high)%nat
sigma high high = f high
    apply sigma_split.f:nat -> R
low, high:nat
H1:(low < high)%nat
H2:(S low <= high)%nat
H3:(low <= high)%nat
H:high = S (Init.Nat.pred high)
(low <= Init.Nat.pred high)%nat
f:nat -> R
low, high:nat
H1:(low < high)%nat
H2:(S low <= high)%nat
H3:(low <= high)%nat
H:high = S (Init.Nat.pred high)
(Init.Nat.pred high < high)%nat
f:nat -> R
low, high:nat
H1:(low < high)%nat
H2:(S low <= high)%nat
H3:(low <= high)%nat
high = S (Init.Nat.pred high)
f:nat -> R
low, high:nat
H1:(low < high)%nat
H2:(S low <= high)%nat
H3:(low <= high)%nat
sigma high high = f high
    apply le_S_n; rewrite <- H; apply lt_le_S; assumption.f:nat -> R
low, high:nat
H1:(low < high)%nat
H2:(S low <= high)%nat
H3:(low <= high)%nat
H:high = S (Init.Nat.pred high)
(Init.Nat.pred high < high)%nat
f:nat -> R
low, high:nat
H1:(low < high)%nat
H2:(S low <= high)%nat
H3:(low <= high)%nat
high = S (Init.Nat.pred high)
f:nat -> R
low, high:nat
H1:(low < high)%nat
H2:(S low <= high)%nat
H3:(low <= high)%nat
sigma high high = f high
    apply lt_pred_n_n; apply le_lt_trans with low; [ apply le_O_n | assumption ].f:nat -> R
low, high:nat
H1:(low < high)%nat
H2:(S low <= high)%nat
H3:(low <= high)%nat
high = S (Init.Nat.pred high)
f:nat -> R
low, high:nat
H1:(low < high)%nat
H2:(S low <= high)%nat
H3:(low <= high)%nat
sigma high high = f high
    apply S_pred with 0%nat; apply le_lt_trans with low;
      [ apply le_O_n | assumption ].f:nat -> R
low, high:nat
H1:(low < high)%nat
H2:(S low <= high)%nat
H3:(low <= high)%nat
sigma high high = f high
    unfold sigma; rewrite <- minus_n_n; simpl;
      replace (high + 0)%nat with high; [ reflexivity | ring ].
  Qed.

  Theorem sigma_eq_arg : forall low:nat, sigma low low = f low.f:nat -> R
forall low : nat, sigma low low = f low
  Proof.f:nat -> R
forall low : nat, sigma low low = f low
    intro; unfold sigma; rewrite <- minus_n_n.f:nat -> R
low:nat
sum_f_R0 (fun k : nat => f (low + k)) 0 = f low
    simpl; replace (low + 0)%nat with low; [ reflexivity | ring ].
  Qed.

End Sigma.