I am interested in understanding how this lemma can be improved (which is part of a bigger proof, see below), as it still seems a bit “long winded” to me. Note I’m not using Mathlib and prefer to stick with Std4 (now Batteries?):

-- A simple proof for "right shifting" bytes.  Suppose a value n which fits
-- within an array of k bytes.  We want to append a new byte in the leftmost
-- position.  This lemma then tells us that the resulting number fits within k+1
-- bytes.
def pow256_shr(n:Nat)(m:UInt8)(k:Nat)(p:n < 256^k) : (m.val * 256^k + n < 256^(k+1)) :=
by
  let l := m.toNat
  --
  have q : l ≤ 255 := by exact Nat.le_of_lt_succ m.val.isLt
  have r : l * 256^k ≤ 255*256^k := by exact Nat.mul_le_mul_right (256 ^ k) q
  have s : l * 256^k + 256^k ≤ 256^(k+1) := by omega
  have t : l * 256^k + n < l * 256^k + 256^k := by
    exact Nat.add_lt_add_left p (l * 256 ^ k)
  exact Nat.lt_of_lt_of_le t s

I was thinking a calc style proof might be better for this, but didn’t manage to make that work. Any thoughts?

Appendix

For reference, I’ve used my lemma above in a proof which bounds the size of a number generated from a list of bytes in big endian notation. Here is that generating function:

def from_bytes_be(bytes:List UInt8) : Nat :=
  match bytes with
  | List.nil => 0
  | b::bs =>
      let n := bs.length
      (b.toNat * (256^n)) + (from_bytes_be bs)

And here is the bounding proof:

-- Bound the number returned by `from_bytes_be`.  For example, if one byte is
-- passed into `from_bytes_be` then the return value is bounded by `256`;
-- likewise, if two bytes are passed into `from_bytes_be` then the return value
-- is bounded by `65536`, etc.
def from_bytes_be_bound(bytes:List UInt8) : (from_bytes_be bytes) < 256^bytes.length :=
by
  match bytes with
  | [] => simp_arith
  | b::bs =>
      apply pow256_shr
      apply (from_bytes_be_bound bs)