It's because it uses a lemma from the Lean4 std (`nat.sub_add_eq_max`) but the online prover is running Lean3
It's because it uses a lemma from the Lean4 std (
nat.sub_add_eq_max) but the online prover is running Lean3