如何改进Lean中pow256_shr引理的证明？（基于Std4/Batteries）

我希望简化以下引理的证明，它是一个更大证明的一部分，目前显得有些冗长。注：我不使用Mathlib，仅使用Std4（即Batteries）。

原引理及证明：

-- 一个关于字节"右移"的简单证明：假设数值 n 能容纳在 k 字节的数组中，
-- 我们在最左侧追加一个新字节，本引理说明结果数值能容纳在 k+1 字节中。
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

我原本想用calc风格的证明，但没能成功实现，请问有什么可行的思路？

附录：相关函数与边界证明 #

作为参考，上述引理用于证明大端字节列表生成数值的大小边界。以下是生成函数：

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)

对应的边界证明：

-- 限制`from_bytes_be`返回值的范围：例如传入1字节时，返回值小于256；
-- 传入2字节时，返回值小于65536，以此类推。
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)

改进思路 #

1. 改用calc风格简化证明

把分步的have整合到calc块中，让逻辑推导链更直观连贯：

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
  calc
    l * 256^k + n < l * 256^k + 256^k := Nat.add_lt_add_left p _
    _ ≤ 255 * 256^k + 256^k := Nat.add_le_add_right (Nat.mul_le_mul_right _ (Nat.le_of_lt_succ m.val.isLt)) _
    _ = (255 + 1) * 256^k := Nat.add_mul _ _ _
    _ = 256 * 256^k := rfl
    _ = 256^(k+1) := Nat.pow_succ _ _

2. 进一步精简步骤

省略临时变量命名，利用Std4的规则合并推导：

def pow256_shr(n:Nat)(m:UInt8)(k:Nat)(p:n < 256^k) : (m.val * 256^k + n < 256^(k+1)) :=
by
  have : m.toNat ≤ 255 := Nat.le_of_lt_succ m.val.isLt
  calc
    m.toNat * 256^k + n < m.toNat * 256^k + 256^k := Nat.add_lt_add_left p _
    _ ≤ 255 * 256^k + 256^k := Nat.add_le_add_right (Nat.mul_le_mul_right _ this) _
    _ = 256^(k+1) := by rw [←Nat.add_mul, Nat.add_one, Nat.pow_succ]; rfl

3. 用omega一步到位（Std4支持场景）

如果Std4的omega策略能识别所有算术规则，可大幅压缩证明：

def pow256_shr(n:Nat)(m:UInt8)(k:Nat)(p:n < 256^k) : (m.val * 256^k + n < 256^(k+1)) :=
by
  have : m.toNat ≤ 255 := Nat.le_of_lt_succ m.val.isLt
  rw [Nat.pow_succ]
  omega

内容的提问来源于stack exchange，提问作者redjamjar