Additions to proof-libs needed for the GCD example

[abentkamp]

While working on verifying the GCD crate, I need to add these definitions and lemmas to the proof-libs.

An open question: Is there a way to generalize over all instances of shift_right_trailing_zeros_nonzero_lemma as I have managed to do for shift_right_le?

And generally, I am not sure if we want these kinds of specific lemmas in the proof-libs.

[maximebuyse]

core::cmp and core::num are already switched to Rust definitions from core models in hax-evit. We shouldn't modify the hand-written F* core lib at this point. @abentkamp could you do a PR to hax-evit instead with modifications to the rust models (and F* rust_primitives)?

[W95Psp]

On the F* side, you could define:

val trailing_zeros: #t:inttype -> int_t t -> (n:u32{v n >= 0 /\ v n <= bits t})

unfold let impl_u8__trailing_zeros (n:u8) = trailing_zeros n
unfold let impl_u16__trailing_zeros (n:u16) = trailing_zeros n
unfold let impl_u32__trailing_zeros (n:u32) = trailing_zeros n
unfold let impl_u64__trailing_zeros (n:u64) = trailing_zeros n
unfold let impl_u128__trailing_zeros (n:u128) = trailing_zeros n
unfold let impl_usize__trailing_zeros (n:usize) = trailing_zeros n

val shift_right_trailing_zeros_nonzero_lemma #t (a: int_t t):
    Lemma (requires (v a <> 0))
          (ensures (v (shift_right a (trailing_zeros a)) <> 0))
          [SMTPat (shift_right a (trailing_zeros a))]

But not clear how this fits the Rust core models story, though.