@@ -310,9 +310,19 @@ fact (S n) = (S n) * fact n
310310-- Division and modulus
311311--------------------------------------------------------------------------------
312312
313+||| The proof that no successor of a natural number can be zero.
314+|||
315+||| ```idris example
316+||| modNatNZ 10 3 SIsNotZ
317+||| ```
313318SIsNotZ : {x: Nat} -> (S x = Z) -> Void
314319SIsNotZ Refl impossible
315320
321+||| Modulus function where the divisor is not zero.
322+|||
323+||| ```idris example
324+||| modNatNZ 100 2 SIsNotZ
325+||| ```
316326modNatNZ : Nat -> (y: Nat) -> Not (y = Z) -> Nat
317327modNatNZ left Z p = void (p Refl)
318328modNatNZ left (S right) _ = mod' left left right
@@ -329,6 +339,11 @@ partial
329339modNat : Nat -> Nat -> Nat
330340modNat left (S right) = modNatNZ left (S right) SIsNotZ
331341
342+||| Division where the divisor is not zero.
343+|||
344+||| ```idris example
345+||| divNatNZ 100 2 SIsNotZ
346+||| ```
332347divNatNZ : Nat -> (y: Nat) -> Not (y = Z) -> Nat
333348divNatNZ left Z p = void (p Refl)
334349divNatNZ left (S right) _ = div' left left right