title: Prove distributive law of multiplication over addition functions in Haskell
body: <p>I'm currently on a beginner's course of haskell and lambda calculus and I'm unsure of how to do the following exercise:</p>
  
  <p>Using the following definitions of (+) and (*) operations in haskell, prove:</p>
  
  <p>1)The distributive law of the (*) over the (+)</p>
  
  <pre><code>(∀m⇓,n⇓,k⇓::N) (m+n) * k = m * k + n * k
  </code></pre>
  
  <p>Definitions:</p>
  
  <pre><code>(+) :: N -&gt; N -&gt; N
  (+) = \m n -&gt; case m of { 0 -&gt; n; S(y) -&gt; S(y+n)}
  
  (*) :: N -&gt; N -&gt; N
  (*) = \m n -&gt; case m of { 0 -&gt; 0; S y -&gt; n + (y*n)}
  </code></pre>
  
  <p>My idea was to do what I did for a previous exercise, prove for each possible case of m. The difference is that the exercise I did was for Boolean type, which can only be true or false and this is a natural, so my guess was to do the proof for the cases m = 0 and m = S(y)</p>
  
  <p>I easily managed to prove the equality for m = 0 but got stuck when doing it for m = S(y)</p>
  
  <p>Case m = 0</p>
  
  <pre><code>(0 + n) * k =? 0 * k + n * k
  Left side:
  (0 + n) * k = (case 0 of {0-&gt;n;Sy-&gt;...}) * k
  = n * k
  Right side:
  0 * k + n * k = (case 0 of {0-&gt;0;Sy-&gt;...}) + (n * k)
  = 0 + (n * k) = (case 0 of {0-&gt;(n*k);Sy-&gt;...}) = n * k (equal to the left side)
  </code></pre>
  
  <p>Case m = S(y)</p>
  
  <pre><code>(Sy + n) * k =? Sy * k + n * k
  Left side:
  (case Sy of {0-&gt;...;Sy-&gt;S(y+n)}) * k = S(y+n) * k
  = case Sx of {0-&gt;...;Sx-&gt; k + k * (y+n)
  Right side:
  Sy * k + n * k = (case Sy of {0-&gt;...;Sy-&gt;k + k*y}) + n * k
  = k + k*y + n * k (Point at which I got stuck)
  </code></pre>
  
  <p>(...) Stands for irrelevant code</p>
  
  <p>On a side question, what exactly does the arrow down ⇓ on ∀m⇓ mean? Thanks in advance!</p>