Proving function defined via well founded recursion

Stream: new members

[erd1]

Hi, I've just started learning lean, and started trying random things, but I can't seem to make the following code work, can someone please help me?

open nat

def f : ℕ → ℕ
| 0 := 0
| (succ n) :=
  have succ n / 2 < succ n, from sorry,
  f (succ n / 2)

lemma lem : f 0 = 0 := rfl

The type checker throws an "type mismatch" error at the lemma below.
Confusingly, this snippet type-checks at https://leanprover.github.io/live/latest/
but not at https://leanprover-community.github.io/lean-web-editor
and I'm quite baffled right now.