pub proof fn lemma_integer_fmt_sound_nonmal_inv()Expand description
ensures
integer_fmt().sound_inv(),integer_fmt().nonmal_inv(),pub proof fn lemma_integer_fmt_sound_nonmal_inv()integer_fmt().sound_inv(),integer_fmt().nonmal_inv(),