Dependently typed FizzBuzz

decBuzzy : (n : Nat) -> Dec (Buzzy n)
decBuzzy Z = Yes ZeroBuzzy
decBuzzy (S Z) = No oneNotBuzzy
decBuzzy (S (S Z)) = No twoNotBuzzy
decBuzzy (S (S (S Z))) = No threeNotBuzzy
decBuzzy (S (S (S (S Z)))) = No fourNotBuzzy
decBuzzy (S (S (S (S (S k))))) with (decBuzzy k)
decBuzzy (S (S (S (S (S k))))) | (Yes prf) = Yes (Buzz prf)
decBuzzy (S (S (S (S (S k))))) | (No way) = No (buzzOff way)