function More(x: int): int {
if x <= 0 then 1 else More(x - 2) + 3
}

lemma {:induction false} Increasing(x: int)
    decreases x
    ensures x < More(x)
{ // 0:
  // x is an int, x can be any value.
    if x <= 0 { // 1: x <= 0 Therefore More(x) == 1 => x <= 0 < 1 == More(x) => x < More(x)
    } else { // 2: Work back to basecase, x > 0 ==> repeated x - 2 eventually enters basecase. 
        Increasing(x-2);
    }
}

method ExampleLemmaUse(a: int) {
    // var b := More(a);
    // Increasing(a);
    // Increasing(b);
    // var c := More(b);
    // assert 2 <= c - a;

    Increasing(a); // this call is along all control paths
    var b := More(a);
    Increasing(b);
    b := More(b);
    // Increasing(b);
    // if a < 1000 {
    //     Increasing(More(a)); // we learn More(a) < More(More(a))
    //     // only here, i.e., when a < 1000
    //     assert 2 <= b - a; // this verifies
    // }
    assert 2 <= b - a; // this does not verify
}