pub proof fn lemma_invert_byte_props(b: u8)Expand description
ensures
invert_byte(b) as nat + b as nat == 0xFF,invert_byte(invert_byte(b)) == b,sign_bit_set(invert_byte(b)) <==> !sign_bit_set(b),