Prelude.lean: fix error on the length of Array.?pad (#4823)

This PR addresses a change not up-streamed in #4822, which implements
(among others) the
`«padRightBytes(_,_,_)_BYTES-HOOKED_Bytes_Bytes_Int_Int»` and
`«padLeftBytes(_,_,_)_BYTES-HOOKED_Bytes_Bytes_Int_Int»` as
`Array.rightpad` and `Array.leftpad` respectively.
However, the length parameter passed to this functions was `Δ :=
len.toNat - b.size`, but it ought to be `len.toNat`, since these
functions pad to the maximum of the length provided.

Co-authored-by: automergerpr-permission-manager[bot] <190534181+automergerpr-permission-manager[bot]@users.noreply.github.com>

Author: JuanCoRo

pyk/src/pyk/klean/template/{{ cookiecutter.package_name }}/{{ cookiecutter.library_name }}/Prelude.lean

@@ -282,16 +282,14 @@ Pads to the right `len - b.length` bytes with specified `val` value
 -/
 def «padRightBytes(_,_,_)_BYTES-HOOKED_Bytes_Bytes_Int_Int» (b : SortBytes) (len val : SortInt) : Option SortBytes :=
   if val < 0 ∨ 255 < val then none else
-  let Δ := len.toNat - b.size
-  some { data := (Array.rightpad Δ (⟨val.toNat⟩ : UInt8) b.data)}
+  some { data := (Array.rightpad len.toNat (⟨val.toNat⟩ : UInt8) b.data)}
 
 /--
 Pads to the left `len - b.length` bytes with specified `val` value
 -/
 def «padLeftBytes(_,_,_)_BYTES-HOOKED_Bytes_Bytes_Int_Int» (b : SortBytes) (len val : SortInt) : Option SortBytes :=
   if val < 0 ∨ 255 < val then none else
-  let Δ := len.toNat - b.size
-  some { data := (Array.leftpad Δ (⟨val.toNat⟩ : UInt8) b.data)}
+  some { data := (Array.leftpad len.toNat (⟨val.toNat⟩ : UInt8) b.data)}
 
 def «lengthBytes(_)_BYTES-HOOKED_Int_Bytes» (x0 : SortBytes) : Option SortInt :=
   Int.ofNat x0.size