// Proofs of summation formulae
import Nat

lemma n_le_nn : all n : Nat. n <= n * n
proof
    induction Nat
    case zero {
        expand operator* | operator <=.
    }
    case suc(n') suppose IH {
      expand operator *
      show suc(n') + ℕ0 ≤ suc(n') + (ℕ0 + n' * (suc(n') + ℕ0))
      have zero_le_any: ℕ0 <= (ℕ0 + n' * (suc(n') + ℕ0))
        by expand operator <=.
      apply add_both_sides_of_less_equal[suc(n')][ℕ0, (ℕ0 + n' * (suc(n') + ℕ0))]
      to zero_le_any
    }
end

lemma blah : all n : Nat.
    n * (n ∸ ℕ1) = n * n ∸ n
proof
    induction Nat
    case zero {
        expand operator∸.
    }
    case suc(n') suppose IH {
      expand operator* | operator∸
      replace monus_zero[n']
                  | add_monus_identity[suc(n')][n' * suc(n')]
                  | mult_commute[n'][suc(n')]
      show n' + n' * n' = suc(n') * n' 
      expand operator*.
    }
end


theorem sum_n : all n : Nat. 
    ℕ2 * summation(n, ℕ0, λ x {x}) = n * (n ∸ ℕ1)
proof
    induction Nat
    case zero {
        evaluate
    }
    case suc(n') suppose IH {
        have step1: (all i:Nat. (if i < ℕ1 then n' + i = ℕ0 + (n' + i)))
            by arbitrary i:Nat
                suppose prem : i < ℕ1
                symmetric zero_add[n'+i]
        suffices n' * (n' ∸ ℕ1) + ℕ2 * summation(ℕ1, n', λn{n}) = (n' + ℕ1) * ((n' + ℕ1) ∸ ℕ1)
            by replace symmetric one_add[n'] | add_commute[ℕ1][n']
            | apply summation_add[n'][ℕ1, ℕ0, n', λn{n}, λn{n}, λn{n}] to step1
            | dist_mult_add[ℕ2][summation(n', ℕ0, λn{n}), summation(ℕ1, n', λn{n})]
            | IH.
        suffices n' * (n' ∸ ℕ1) + ℕ2 * (n' + ℕ0) = (n' + ℕ1) * ((n' + ℕ1) ∸ ℕ1)
            by expand 2*summation.
        suffices n' * (n' ∸ ℕ1) + ℕ2 * n' = suc(n') * (suc(n') ∸ ℕ1)
              by replace add_one[n'].
        suffices (n' * n' ∸ n') + (n' + n') = suc(n') * n' by {
          expand operator∸
          replace monus_zero[n'] | blah[n'] | two_mult[n'].
        }
        suffices ((n' * n' ∸ n') + n') + n' = n' + n' * n' by expand operator*.
        suffices n' * n' + n' = n' + n' * n' by 
            replace add_commute[(n' * n' ∸ n')][n']
            | apply monus_add_identity[n'*n'][n'] to n_le_nn[n'].
        add_commute[n' * n'][n']
    }
end

theorem sum_n' : all n : Nat. 
    ℕ2 * summation(suc(n), ℕ0, λ x {x}) = n * (n + ℕ1)
proof
    induction Nat
    case zero {
      expand 2* summation.
    }
    case suc(n') suppose IH {
        have step1: (all i:Nat. (if i < ℕ1 then suc(n') + i = ℕ0 + (suc(n') + i)))
            by arbitrary i:Nat
                suppose prem : i < ℕ1
                symmetric zero_add[suc(n')+i]
        
        replace symmetric one_add[n'] | add_commute[ℕ1][n']
               | symmetric add_one[n' + ℕ1] | add_one[n']
               |  apply summation_add[suc(n')][ℕ1, ℕ0, suc(n'), λn{n}, λn{n}, λn{n}] to step1
               | dist_mult_add[ℕ2][summation(suc(n'), ℕ0, λn{n}), summation(ℕ1, suc(n'), λn{n})]
               | IH
        show n' * (n' + ℕ1) + ℕ2 * summation(ℕ1, suc(n'), λn{n}) = suc(n') * (suc(n') + ℕ1)
        suffices n' * (n' + ℕ1) + ((n' + ℕ1) + (n' + ℕ1)) = (n' + ℕ1) * ((n' + ℕ1) + ℕ1) by {
          expand 2* summation
          replace two_mult[suc(n')] | symmetric add_one[n'].
        }
        suffices (n' * n' + n') + ((n' + ℕ1) + (n' + ℕ1))
               = ((n' * n' + n') + (n' + ℕ1)) + (n' + ℕ1) by {
          replace dist_mult_add[n' + ℕ1][n' + ℕ1, ℕ1]
          | dist_mult_add[n'][n', ℕ1]
          | dist_mult_add[n' + ℕ1][n', ℕ1]
          | dist_mult_add_right[n', ℕ1, n'].
        }
        .
    }
end