{-
`equal` checks if two Naturals are equal.
-}
let equal
    : Natural → Natural → Bool
    =   λ(a : Natural)
      → λ(b : Natural)
      →     Natural/isZero (Natural/subtract a b)
        &&  Natural/isZero (Natural/subtract b a)

let example0 = assert : equal 5 5 ≡ True

let example1 = assert : equal 5 6 ≡ False

in  equal