Function lemma_nat_from_be_bytes_fits_usize 

pub proof fn lemma_nat_from_be_bytes_fits_usize(bytes: Seq<u8>)

requires

bytes.len() <= size_of_usize(),

ensures

nat_from_be_bytes(bytes) <= usize::MAX,