calc
  append I L S ‖I‖ X = S % I # L + X * I # L := by simp [append, bexp_eq_hash]
  _                  < (X + 1) * I # L       := by simp [add_mul, add_comm]
  _                  ≤ L # 1 * I # L         := mul_le_mul_right (succ_le_iff_lt.mpr $ lt_hash_one_iff.mpr hX)
  _                  ≤ (I # L) ^ 2           := by simp [sq, hash_comm L 1]; exact hash_monotone (pos_iff_one_le.mp Ipos) (by rfl)
case inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
I L S X : M
hX : ‖X‖ ≤ ‖L‖
Ipos : 0 < I
⊢ append I L S ‖I‖ X < (I # L) ^ 2
no goals