title: Proving a type empty in Agda
body: <p>I am trying to prove 2*3!=5 in agda.  To do this I will define a function with a signature 2 * 3 ≡ 5 → ⊥.</p>
  
  <p>making use of my definition of multiplication </p>
  
  <pre><code>data _*_≡_ : ℕ → ℕ → ℕ → Set where
    base : ∀ {n} → 0 * n ≡ 0
    succ : ∀ {n m k j} → m * n ≡ j → j + n ≡ k → suc m * n ≡ k
  </code></pre>
  
  <p>I have proven</p>
  
  <pre><code>1*3≡3 : 1 * 3 ≡ 3
  1*3≡3 = (succ base) znn
  </code></pre>
  
  <p>and</p>
  
  <pre><code>3+3≡5 : 3 + 3 ≡ 5 → ⊥
  3+3≡5 (sns (sns (sns ())))
  </code></pre>
  
  <p>But when I try to prove:</p>
  
  <pre><code>m235 : 2 * 3 ≡ 5 → ⊥
  m235 ( ( succ  1*3≡3 ) ( x ) ) = ( 3+3≡5 x )
  </code></pre>
  
  <p>the compiler spits out this error about x</p>
  
  <pre><code>.j != (suc 2) of type ℕ
  when checking that the expression x has type 3 + 3 ≡ 5
  </code></pre>
  
  <p>Sorry if this is a stupid question.  Thanks in advance.</p>