structure NZ where
  n  : Int
  ne : n ≠ 0

def safeDiv (n1 : Int) (n2 : NZ) : Int := n1 / n2.n

-- 5
#eval safeDiv 10 ⟨2, by decide⟩
-- 5
#eval safeDiv 10 ⟨1 + 1, by decide⟩
-- error: 0 ≠ 0 is false
-- #eval safeDiv 10 ⟨0, by decide⟩
-- error: 1 + -1 ≠ 0 is false
-- #eval safeDiv 10 ⟨1 + -1, by decide⟩


-- The proof can use facts about variables.
def f (a : Int) (h : a > 0) : Int := safeDiv 10 ⟨a + 1, by omega⟩
def g (a : Int) (h : a > -1) : Int := safeDiv 10 ⟨a + 1, by omega⟩
-- error
-- def k (a : Int) (h : a > -2) : Int := safeDiv 10 ⟨a + 1, by omega⟩

-- We can use tests to provide proofs.
def tryDiv (n1 n2 : Int) : Except String Int :=
  if h : n2 ≠ 0 then .ok (safeDiv n1 ⟨n2, h⟩) else .error "divide by zero"
-- To see the proof that is passed, replace h with _ and read the error.

-- Except.ok 5
#eval tryDiv 10 2
-- Except.error "divide by zero"
#eval tryDiv 10 0