Allow decreases classes to prove termination

[karthikbhargavan]

In recursive functions like the following, F* is not able to automatically prove termination.

fn f(x:usize, n:usize) { 
    if x < n {
        f (x+1,n)
    }
}

Open this code snippet in the playground

Consequently, we would like to be able to annotate the Rust code with a decreases clause of the form:

#[hax_lib::decreases(n - x)]

This would allow F* to automatically prove termination.