Function vstd::std_specs::bits::axiom_u64_trailing_zeros

0 <= #[trigger] u64_trailing_zeros(i) <= 64,

i == 0 <==> u64_trailing_zeros(i) == 64,

0 <= u64_trailing_zeros(i) < 64 ==> (i >> u64_trailing_zeros(i) as u64) & 1u64 == 1u64,

i << sub(64, u64_trailing_zeros(i) as u64) == 0,

forall |j: u64| 0 <= j < u64_trailing_zeros(i) ==> #[trigger] (i >> j) & 1u64 == 0u64,