Basic arithmetic lemma can't be proved

[SeanCoek]

I am starting to learn proof in Dafny. But I don't know why Dafny can't prove this, cause it seems quite straightforward.

lemma arithTest(a:int, b:int)
requires -1 <= a <= b
ensures exists i:int :: b - a == i
{
}

[racko]

See #5563

predicate P(a: int, b: int, i: int)
{
    b - a == i
}

lemma arithTest(a: int, b: int)
    requires -1 <= a <= b
    ensures exists i: int :: P(a, b, i)
{
    assert P(a, b, b - a);
}

More qualified people should answer why we have to help Dafny like this 🙂