You are an expert Lean4 and formal verification agent proving a Lean4 theorem. Your output **must** strictly adhere to the specified format.

### Input Information
You will receive the following components, relevant to the target theorem:
* <all_available_defs>: Definitions available from imported modules (either from the current Lean repository or from Mathlib)
* <all_available_lemmas>: Lemmas/theorems available that may assist the proof.
* <local_ctx>...</local_ctx>: The local file context (imports, namespaces, definitions, comments, etc.) from the top of the file up to—but not including—the target theorem or any previously defined local lemmas/theorems.
* <target_theorem>...</target_theorem>: The target theorem statement, ending with `:=`.

**Notes**
1. Definitions include their full bodies, but for definitions whose bodies contain proofs, the proof parts are replaced by `admit` (i.e., admit /- proof elided -/), while the rest of the definition is kept unchanged; lemmas include only their statements.
2. You may freely reference any definition or lemma contained in these tags without redefining them.
3. The tags for available definitions and lemmas (all_available_defs, all_available_lemmas) may be omitted if empty.

### Output Format & Requirements
Your output MUST contain a complete, syntactically correct Lean 4 proof for the target theorem.

**Strict Output Structure:**
<reasoning> 
...
</reasoning> 

<lean4_invented_lemmas>
-- each lemma is a full Lean 4 declaration with a complete proof
...
</lean4_invented_lemmas>

<lean4_proof>
-- Lean 4 proof body of the target theorem
...
</lean4_proof>

**Requirements:**
1. <reasoning> and <lean4_invented_lemmas> are OPTIONAL. Include them only if they aid proof construction.
2. <lean4_proof> MUST contain only the proof body (tactics/terms), starting by "by", NOT the theorem declaration.
3. <lean4_invented_lemmas> (if present) MUST contain syntactically correct lemma declarations that type checks AND complete proof bodies. Defining a lemma using `axiom` is NOT allowed.
4. <reasoning> contains high-level proof planning.
5. If you create a lemma under <lean4_invented_lemmas> whose name is namespaced (e.g., X.Y.Z), you MUST always refer to it using its fully qualified name. Do NOT rely on shortened names. For example, write rw [X.Y.Z], not rw [Z] for invented lemmas.
6. All Lean 4 code MUST be syntactically correct. No `sorry`, `admit`, or non-Lean text. Comments allowed using `--` or `/- ... -/`.
7. Follow the tags and structure EXACTLY. No extra text before, between, or after the sections.
8. Do NOT wrap invented lemmas in a `mutual` block unless they have genuine mutual recursion. Declare each lemma independently.

### Examples are provided here (example input are under "User Prompt", and example assistant response are under "Agent Response"):
Example 1 ------------------- 
User Prompt:
<all_available_defs>
structure BitVec (w : Nat) where
  /-- Construct a `BitVec w` from a number less than `2^w`.
  O(1), because we use `Fin` as the internal representation of a bitvector. -/
  ofFin ::

  /-- Interpret a bitvector as a number less than `2^w`.
  O(1), because we use `Fin` as the internal representation of a bitvector. -/
  toFin : Fin (hPow 2 w)
</all_available_defs>

<all_available_lemmas>
theorem List.getElem_append_left{α : Type u_1} {l₁ l₂ : List α} {i : Nat} (hn : i < l₁.length) : (l₁ ++ l₂)[i] = l₁[i]
theorem getElem_eq_testBit_toNat (x : BitVec w) (i : Nat) (h : i < w) :
  x[i] = x.toNat.testBit i := rfl
@[simp, grind =] theorem toNat_cons (b : Bool) (x : BitVec w) :
    (cons b x).toNat = (b.toNat <<< w) ||| x.toNat
@[simp, grind =] theorem getLsbD_of_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : getLsbD x i = false
theorem testBit_toNat (x : BitVec w) : x.toNat.testBit i = x.getLsbD i
</all_available_lemmas>

<local_ctx>
import Mathlib.Computability.NFA
import Mathlib.Data.FinEnum
import Mathlib.Data.Rel
import Mathlib.Data.Vector.Basic
import Blase.AutoStructs.ForLean

open Set
open Mathlib
open SetRel

-- this is better because card is defeq to n
instance (α : Type) : Inter (Language α) := ⟨Set.inter⟩
instance (α : Type) : Union (Language α) := ⟨Set.union⟩

/--
The set of `n`-tuples of bit vectors of an arbitrary width.
-/
structure BitVecs (n : Nat) where
  w : Nat
  bvs : List.Vector (BitVec w) n

def BitVecs.cast (bvs : BitVecs n) (h : n = n') : BitVecs n' :=
  { w := bvs.w, bvs := h ▸ bvs.bvs }

abbrev BitVecs.empty : BitVecs n := ⟨0, List.Vector.replicate n .nil⟩
abbrev BitVecs.singleton {w : Nat} (bv : BitVec w) : BitVecs 1 := ⟨w, bv ::ᵥ .nil⟩
abbrev BitVecs.pair {w : Nat} (bv1 bv2 : BitVec w) : BitVecs 2 := ⟨w, bv1 ::ᵥ bv2 ::ᵥ .nil⟩

/--
The set of `n`-tuples of bit vectors of an arbitrary width, encoded as a list of
bit vectors of width `n`. The width of the encoded bit vectors is the length of
the list.
-/
abbrev BitVecs' (n : Nat) := List (BitVec n)

@[simps]
def dec (bvs' : BitVecs' n) : BitVecs n where
  w := bvs'.length
  bvs := List.Vector.ofFn fun k => BitVec.ofFn fun i => bvs'[i].getLsbD k

@[simp]
</local_ctx>

<target_theorem>
lemma dec_snoc n (bvs' : BitVecs' n) (a : BitVec n) :
  dec (bvs' ++ [a]) =
    { w := bvs'.length + 1
      bvs := List.Vector.ofFn fun k =>
        BitVec.cons (a.getLsbD k) ((dec bvs').bvs.get k) } :=
</target_theorem>

Agent Response:
<reasoning> 
The goal is to understand what `dec` does after appending one more bitvector `a` to `bvs'`. By definition, `dec` builds a width `= length` and a vector of bitvectors whose `i`-th bit at position `k` is `bvs'[i].getLsbD k`. So for `bvs' ++ [a]`, we expect the width to increase by 1 and each resulting bitvector to be `BitVec.cons` of the new bit coming from `a`.

First, I use `ext` twice: once on the record to focus on the `bvs` field, and once on the resulting bitvector. This reduces everything to a pointwise statement:
for fixed `k` and `i` with `i < bvs'.length + 1`,
the bit `(bvs' ++ [a])[i].getLsbD k` should match the bit at index `i` of `BitVec.cons (a.getLsbD k) ((dec bvs').bvs.get k)`.

At this point I need a clean description of indexing into `BitVec.cons`: if we have `x : BitVec n`, then `(cons b x)[i]` should give `b` at the new “last” index `n` and `x[i]` otherwise. That motivates an auxiliary lemma `getElem_cons` expressing exactly this behavior, proved via the `testBit`/`toNat` characterization and a case split on `i < n`, `i = n`, `i > n`.

Using `getElem_cons`, the RHS becomes an `if` on whether `i = bvs'.length`. So I split into cases:
- If `i = bvs'.length`, then `(bvs' ++ [a])[i]` is the appended `a`, so both sides reduce to `a.getLsbD k`.
- If `i ≠ bvs'.length`, the bound `i < bvs'.length + 1` forces `i < bvs'.length`. Then `(bvs' ++ [a])[i] = bvs'[i]` by `List.getElem_append_left`, and the RHS takes the “else” branch and likewise gives the bit from `bvs'[i]`. In both subcases, `simp` (plus the definition of `dec`) finishes.

So the whole proof is: `ext` to bit level, unfold `dec` with `simp_all`, rewrite with `getElem_cons`, split on the boundary index `i = length bvs'`, and in the “< length” branch use `List.getElem_append_left` and bounds to line up both sides.
</reasoning> 

<lean4_invented_lemmas>
@[grind =]
theorem getElem_cons {b : Bool} {n} {x : BitVec n} {i : Nat} (h : i < n + 1) :
    (cons b x)[i] = if h : i = n then b else x[i] := by
  simp only [BitVec.getElem_eq_testBit_toNat, BitVec.toNat_cons, Nat.testBit_or]
  rw [Nat.testBit_shiftLeft]
  rcases Nat.lt_trichotomy i n with i_lt_n | i_eq_n | n_lt_i
  · have p1 : ¬(n ≤ i) := by omega
    have p2 : i ≠ n := by omega
    simp [p1, p2]
  · simp only [i_eq_n, ge_iff_le, Nat.le_refl, decide_true, Nat.sub_self, Nat.testBit_zero,
    Bool.true_and, BitVec.testBit_toNat, BitVec.getLsbD_of_ge, Bool.or_false]
    cases b <;> trivial
  · have p1 : i ≠ n := by omega
    have p2 : i - n ≠ 0 := by omega
    simp [p1, p2, Nat.testBit_bool_toNat]
</lean4_invented_lemmas>

<lean4_proof>
by
  ext k i hi <;> simp_all
  rw [getElem_cons]
  split
  next heq => simp_all
  next h =>
    have hlt : i < List.length bvs' := by simp at hi; omega
    rw [List.getElem_append_left hlt]
    simp
</lean4_proof>

### Your task:
<all_available_defs>
def Wad : Type := UInt128

instance : Inhabited Wad := ⟨default (α := UInt128)⟩

def WAD_SCALE : ℕ := 1000000000000000000

protected def toZMod : UInt128 := w

protected def ofZMod (a : UInt128) : Wad := a

protected def toRat : ℚ := w.toZMod.val / WAD_SCALE

protected def mul : Wad := (w.toZMod.val * w'.toZMod.val / WAD_SCALE : UInt128)

instance : Mul Wad := ⟨Wad.mul⟩

protected def div : Wad := (w.toZMod.val * WAD_SCALE / w'.toZMod.val : UInt128)

instance : Div Wad := ⟨Wad.div⟩

protected def sub : Wad := w.toZMod - w'.toZMod

instance : Sub Wad := ⟨Wad.sub⟩

protected def add : Wad := w.toZMod + w'.toZMod

instance : Add Wad := ⟨Wad.add⟩

protected def zero : Wad := (0 : UInt128)

instance : Zero Wad := ⟨Wad.zero⟩

protected def one : Wad := (1000000000000000000 : UInt128)

instance : One Wad := ⟨Wad.one⟩

def Ray : Type := UInt128

instance : Inhabited Ray := ⟨default (α := UInt128)⟩

def RAY_SCALE : ℕ := 1000000000000000000000000000

protected def toZMod : UInt128 := r

protected def ofZMod (a : UInt128) : Ray := a

protected def toRat : ℚ := r.toZMod.val / RAY_SCALE

protected def mul : Ray := (r.toZMod.val * r'.toZMod.val / RAY_SCALE  : UInt128)

instance : Mul Ray := ⟨Ray.mul⟩

protected def div : Ray := (r.toZMod.val * RAY_SCALE / r'.toZMod.val : UInt128)

instance : Div Ray := ⟨Ray.div⟩

def DIFF : ℕ := 1000000000

def toWad : Wad := r.toZMod.ndiv DIFF

protected def add : Ray := r.toZMod + r'.toZMod

instance : Add Ray := ⟨Ray.add⟩

protected def sub : Ray := r.toZMod - r'.toZMod

instance : Sub Ray := ⟨Ray.sub⟩

protected def zero : Ray := (0 : UInt128)

instance : Zero Ray := ⟨Ray.zero⟩

protected def one : Wad := (1000000000000000000000000000 : UInt128)

instance : One Ray := ⟨Ray.one⟩

def Wad.toRay (w : Wad) : Ray := w.toZMod * (Ray.DIFF : UInt128)

def Wad.MAX_CONVERTIBLE_WAD : ℕ := 340282366920938463463374607431

def SignedWad := UInt128 × (Unit ⊕ Unit)

instance : Inhabited SignedWad := ⟨default, default⟩

def sign : ℤ := if SierraBool.toBool w.2 then -1 else 1

instance : Zero SignedWad := ⟨(0, false.toSierraBool)⟩

instance : One SignedWad := ⟨(Wad.WAD_SCALE, false.toSierraBool)⟩

def toRat : ℚ := if w.2 then -(Wad.toRat w.1) else Wad.toRat w.1

protected def mul : SignedWad :=
⟨Wad.mul (w₁.1 : Wad) (w₂.1 : Wad), Bool.toSierraBool (Bool.xor (SierraBool.toBool w₁.2) (SierraBool.toBool w₂.2))⟩

instance : Mul SignedWad := ⟨SignedWad.mul⟩

protected def div : SignedWad :=
⟨Wad.div (w₁.1 : Wad) (w₂.1 : Wad), Bool.toSierraBool (Bool.xor (SierraBool.toBool w₁.2) (SierraBool.toBool w₂.2))⟩

instance : Div SignedWad := ⟨SignedWad.div⟩

def SignedRay := UInt128 × (Unit ⊕ Unit)

instance : Inhabited SignedRay := ⟨default, default⟩

def sign : ℤ := if SierraBool.toBool w.2 then -1 else 1

instance : Zero SignedRay := ⟨(0, false.toSierraBool)⟩

instance : One SignedRay := ⟨(Ray.RAY_SCALE, false.toSierraBool)⟩

def toRat : ℚ := if SierraBool.toBool w.2 then -(Ray.toRat w.1) else Ray.toRat w.1

protected def mul : SignedRay :=
⟨Ray.mul w₁.1 w₂.1, Bool.toSierraBool (Bool.xor (SierraBool.toBool w₁.2) (SierraBool.toBool w₂.2))⟩

instance : Mul SignedRay := ⟨SignedRay.mul⟩

protected def div : SignedRay :=
⟨Ray.div (w₁.1 : Ray) (w₂.1 : Ray), Bool.toSierraBool (Bool.xor (SierraBool.toBool w₁.2) (SierraBool.toBool w₂.2))⟩

instance : Div SignedRay := ⟨SignedRay.div⟩

Sierra.PRIME in Aegis.Types

Sierra.U128_MOD in Aegis.Types

Sierra.F in Aegis.Types

Sierra.UInt128 in Aegis.Types

Bool in Init.Prelude

Bool.toSierraBool in Aegis.Aux.Bool

Int in Init.Data.Int.Basic

Nat in Init.Prelude

Option in Init.Prelude

Sierra.aegis_prove in Aegis.Commands

Sum in Init.Core

Sum.inl in Init.Core

ZMod in Mathlib.Data.ZMod.Defs

NeZero in Init.Data.NeZero

ZMod.cast in Mathlib.Data.ZMod.Basic

ZMod.val in Mathlib.Data.ZMod.Basic

Function.Injective in Init.Data.Function

cast in Init.Prelude

Ring in Mathlib.Algebra.Ring.Defs

Fin in Init.Prelude

Nat.cast in Init.Data.Cast

NatCast in Init.Data.Cast

NatCast.natCast in Init.Data.Cast

ZMod.valMinAbs in Mathlib.Data.ZMod.ValMinAbs

Inhabited in Init.Prelude

Rat in Init.Data.Rat.Basic

Mul in Init.Prelude

Div in Init.Prelude

Sub in Init.Prelude

Add in Init.Prelude

Zero in Init.Prelude

One in Init.Prelude

Unit in Init.Prelude

SierraBool.toBool in Aegis.Aux.Bool

Bool.xor in Init.Data.Bool

Sierra.U256_MOD in CorelibVerification.Aux.UInt256

List in Init.Prelude

Sierra.UInt256 in CorelibVerification.Aux.UInt256

sierra_simp' in CorelibVerification.Corelib.Integer

Prod in Init.Prelude

Prod.mk in Init.Prelude

Sum.inr in Init.Core

ZMod.ndiv in Aegis.Aux.ZMod.DivMod
</all_available_defs>

<all_available_lemmas>
theorem Bool.toSierraBool_def (b : Bool) : b.toSierraBool = if b then .inr () else .inl ()

theorem U128_MOD_lt_U256_MOD : U128_MOD < U256_MOD

theorem WAD_SCALE_val : (1000000000000000000 : UInt128).val = 1000000000000000000 := rfl

aegis_spec "wadray::wadray::u128_wmul"

theorem RAY_SCALE_val :
    (1000000000000000000000000000 : UInt128).val = 1000000000000000000000000000 := rfl

aegis_spec "wadray::wadray::u128_rmul"

theorem two_U128_MOD_lt_PRIME : 2 * U128_MOD < PRIME

theorem four_U128_MOD_lt_PRIME : 4 * U128_MOD < PRIME

theorem four_U128_MOD_le_PRIME : 4 * U128_MOD ≤ PRIME

theorem add_aux1 (x : UInt128) : 4 * (x.cast : F).valMinAbs.natAbs < PRIME
</all_available_lemmas>

<local_ctx>
import CorelibVerification.Aux.ZMod

import Aegis.Aux.Bool

import Aegis.Aux.ZMod.DivMod

open Sierra

def Wad : Type := UInt128

namespace Wad

def WAD_SCALE : ℕ := 1000000000000000000

variable (w w' : Wad)

protected def toZMod : UInt128 := w

protected def toRat : ℚ := w.toZMod.val / WAD_SCALE

end Wad

def Ray : Type := UInt128

namespace Ray

variable (r r' : Ray)

protected def toZMod : UInt128 := r

end Ray

def SignedWad := UInt128 × (Unit ⊕ Unit)

namespace SignedWad

variable (w w₁ w₂ : SignedWad)

def toRat : ℚ := if w.2 then -(Wad.toRat w.1) else Wad.toRat w.1
</local_ctx>

<target_theorem>
theorem val_eq_zero_of_toRat_neg (x : Wad) (p q : Unit)
  (h : SignedWad.toRat ((x, .inl p) : SignedWad) = SignedWad.toRat ((x, .inr q) : SignedWad)) :
    x = 0 :=
</target_theorem>

