Haskell Demonstration Induction and Recursion

1) I need to demonstrate that cut function is fulfilled (∀list:: [a])(∀x :: a) cut x (cut x list) = 0

cut :: Eq a => a -> [a] -> [a]
cut = a -> l -> case a of {
y -> case l of {
[] -> [];
(x:xs) -> if x == y then [] else [x] ++ (cut a xs);
};
}

2) I need to demonstrate that (∀list:: [a])(∀x :: a)(∀y :: a) count x (count y list) ≤ count x list.

count :: Eq a => a -> [a] -> N
count = a -> l -> case a of {
y -> case l of {
[] -> O;
(x:xs) -> if x == y then S(count a xs) else (count a xs);
};
}

—————————–

{- This is the data type of natural numbers which you have to use: -}

{-#LANGUAGE GADTs #-}
{-# OPTIONS_GHC -fno-warn-tabs #-}
{-# OPTIONS_GHC -fno-warn-missing-methods #-}

module Naturales where

import Prelude hiding (Eq, (==), (/=), Ord, (<),(),(>=))
import Data.Eq

data N where { O :: N ;
S :: N -> N
} deriving Show

one :: N
one = S O

two :: N
two = S one

three :: N
three = S two

four :: N
four = S three

five :: N
five = S four

six :: N
six = S five

seven :: N
seven = S six

eight:: N
eight = S seven

nine:: N
nine= S eight