Why Verus cannot auto infer "j -1" is nat given that j > 0?

[KaminariOS]

spec fn fibo(n: nat) -> nat
    decreases n,
{
    if n == 0 {
        0
    } else if n == 1 {
        1
    } else {
        fibo((n - 2) as nat) + fibo((n - 1) as nat)
    }
}

I wrote this:

proof fn lemma_fibo_is_monotoni1( j: nat)
    requires j > 0
    ensures fibo(j) >= fibo(j - 1)
{
    assert(j - 1 >= 0);
        reveal_with_fuel(fibo, 2);
    // if j < 2 {
    // } else  {
    //     assert(fibo(j ) >= fibo(j - 1));
    //     }
}

Error says j - 1 is int.
It seems that Verus can auto infer j + 1 is nat but for j - 1 I need to use as nat to tell Verus it is a nat.

[Chris-Hawblitzel]

The reason for this is that Verus relies on the standard Rust type checker for types like int and nat, and the Rust type checker does not reason about integer arithmetic when performing type checking (in contrast to Verus verifier, which uses an SMT solver to reason about integer arithmetic when performing verification). Because of this, the typing rules that Verus encodes for operations on int and nat are conservative -- they can assume that adding two nat values produces a nat, but subtracting two nat values might yield a negative number. (I've found that this often makes nat less convenient than int.)

[utaal]

@KaminariOS for questions like this, I also recommend asking on Zulip: https://verus-lang.zulipchat.com/login/
I'll close as resolved, but feel free to reopen if you have further questions. Thanks @Chris-Hawblitzel!