the whole first solution

fizzbuzz.idr

||| proof that k is divisible by 3, can only be called when the compiler can verify it
IsFizz : (k : Nat) -> Type
IsFizz k = (modNatNZ k 3 SIsNotZ = 0)   -- modNatNZ is modulos for natural numbers except for 0. 
-- SIsNotZ is also a proof about k in this case. Compiler will fail if k is not greater than 0

IsBuzz : Nat -> Type
IsBuzz k = (modNatNZ k 5 SIsNotZ = 0)

||| There are four constructors : Fizz, Buzz, FizzBuzz, and Normal. 
||| Every constructor takes two arguments then returns an instance of "Fizzbuzz k"
data Fizzbuzz : (k: Nat) -> Type where
  Fizz : (k: Nat) -> (IsFizz k) -> Not (IsBuzz k) -> Fizzbuzz k
  Buzz : (k: Nat) -> Not (IsFizz k) -> IsBuzz k -> Fizzbuzz k
  FizzBuzz : (k: Nat) -> IsFizz k -> IsBuzz k -> Fizzbuzz k
  Normal : (k: Nat) -> Not (IsFizz k) -> Not (IsBuzz k) -> Fizzbuzz k

||| the public function taking a natural number and returning a FizzBuzz
fizzbuzz : (k: Nat) -> Fizzbuzz k
-- implementation removed for brievity

showFizzBuzz : Nat -> String
-- implementation removed for brievity