[Agda] Matching problem at end of equational reasoning proof

[Christoph Herrmann]

Hi,

I have attached an inductive proof (attempt) of Gauss' summation formula.

The problem is that at the end of the equational reasoning the matching
with the right-hand side of the type does not seem to work, namely:

(suc n) * ((suc n) + 1) against (a * (a + 1)) in the case that a=(suc n)

I am wondering whether Agda still knows that it is in the case a=(suc n)
or whether this information is available only for matching the left-hand 
side.

The error message is:

Gauss.agda:42,4-43,3
n + 1 != n of type ℕ
when checking that the expression (suc n * (suc n + 1) ∎) has type
.Relation.Binary.PreorderReasoning._IsRelatedTo_
(.Relation.Binary.EqReasoning._.preorder Data.Nat.setoid)
(suc (n + (n + 1) * suc n)) (_49 n)

Cheers
-------------- next part --------------
module Gauss where

open import Algebra
open import Data.Nat 
open import Data.Nat.Properties
import Relation.Binary.EqReasoning 
open Relation.Binary.EqReasoning (Data.Nat.setoid)
open import Relation.Binary.PropositionalEquality using (cong)
open Algebra.CommutativeSemiring commutativeSemiring 
        hiding (_+_; _*_)
        renaming (zero to *-zero) 

sum : ℕ -> ℕ
sum 0 = 0
sum (suc n) = suc n + sum n

gauss-formula : ∀ {a : ℕ} -> (2 * sum a ≈ a * (a + 1))
gauss-formula {0} =
 begin
   2 * sum 0
 ≈⟨ cong (λ p → 2 * p) refl ⟩
   2 * 0
 ≈⟨ refl ⟩
   0 * (0 + 1)
 ∎
gauss-formula {suc n} =
 begin
  2 * sum (suc n) 
 ≈⟨ cong (λ p → 2 * p) refl ⟩
  2 * (suc n + sum n)
 ≈⟨ refl ⟩
  2 * suc n + 2 * sum n
 ≈⟨ cong (λ p -> 2 * suc n + p) (gauss-formula {n}) ⟩
  2 * suc n + (n * (n + 1))
 ≈⟨ refl ⟩
  2 * (n + 1) + n * (n + 1)
 ≈⟨ refl ⟩
  (2 + n) * (n + 1)
 ≈⟨ refl ⟩
  ((suc n) + 1) * (suc n)
 ≈⟨ refl ⟩
  (suc n) * ((suc n) + 1)
 ∎