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:
* <used_lib_defs>...</used_lib_defs>: Imported library definitions directly used by the theorem.
* <used_repo_defs>...</used_repo_defs>: Definitions from the local project (but outside the current file), directly or transitively used by the theorem.
* <lib_lemmas>...</lib_lemmas>: Imported library lemmas/theorems that may assist the proof.
* <repo_lemmas>...</repo_lemmas>: Lemmas/theorems defined in the local project outside this file.
* <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 used definitions and helpful lemmas (used_lib_defs, used_repo_defs, lib_lemmas, repo_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:
<used_lib_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)
</used_lib_defs>

<repo_lemmas>
theorem List.getElem_append_left{α : Type u_1} {l₁ l₂ : List α} {i : Nat} (hn : i < l₁.length) :\n(l₁ ++ l₂)[i] = l₁[i]
</repo_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:
<used_lib_defs>
Sierra.UInt128 in Aegis.Types
Unit in Init.Prelude
Bool in Init.Prelude
Bool.toSierraBool in Aegis.Aux.Bool
Bool.xor in Init.Data.Bool
SierraBool.toBool in Aegis.Aux.Bool
Sierra.F in Aegis.Types
Sierra.PRIME in Aegis.Types
Int in Init.Data.Int.Basic
Nat in Init.Prelude
Option in Init.Prelude
Sierra.U128_MOD in Aegis.Types
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
Inhabited in Init.Prelude
</used_lib_defs>

<used_repo_defs>
def RAY_SCALE : ℕ := 1000000000000000000000000000

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

def SignedRay := UInt128 × (Unit ⊕ Unit)

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

def Ray : Type := UInt128

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

def WAD_SCALE : ℕ := 1000000000000000000

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

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

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

def Wad : Type := UInt128

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

protected def toZMod : UInt128 := w

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

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

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

protected def toZMod : UInt128 := r

def DIFF : ℕ := 1000000000

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

def SignedWad := UInt128 × (Unit ⊕ Unit)

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

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

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

<lib_lemmas>
le_of_lt in Mathlib.Order.Defs.PartialOrder
Int.cast_abs in Mathlib.Algebra.Order.Ring.Cast
Int.cast_add in Mathlib.Data.Int.Cast.Basic
Int.cast_natAbs in Mathlib.Algebra.Order.Ring.Cast
Int.cast_neg in Mathlib.Data.Int.Cast.Basic
Int.natAbs_neg in Init.Data.Int.Order
Nat.abs_cast in Mathlib.Data.Nat.Cast.Order.Ring
Nat.cast_add in Mathlib.Data.Nat.Cast.Defs
Nat.cast_le in Mathlib.Data.Nat.Cast.Order.Basic
Nat.cast_lt in Mathlib.Data.Nat.Cast.Order.Basic
Nat.mul_lt_mul_of_pos_left in Init.Data.Nat.Basic
SierraBool_toBool_inl in Aegis.Aux.Bool
SierraBool_toBool_inr in Aegis.Aux.Bool
Sum.getLeft?_inl in Init.Data.Sum.Basic
Sum.getLeft?_inr in Init.Data.Sum.Basic
Sum.isLeft_inl in Init.Data.Sum.Basic
Sum.isLeft_inr in Init.Data.Sum.Basic
Sum.isRight_inl in Init.Data.Sum.Basic
Sum.isRight_inr in Init.Data.Sum.Basic
ZMod.intCast_cast in Mathlib.Data.ZMod.Basic
ZMod.natCast_val in Mathlib.Data.ZMod.Basic
ZMod.valMinAbs_neg_of_ne_half in Mathlib.Data.ZMod.ValMinAbs
ZMod.val_lt in Mathlib.Data.ZMod.Basic
abs_div in Mathlib.Algebra.Order.Field.Basic
abs_neg in Mathlib.Algebra.Order.Group.Unbundled.Abs
add_div in Mathlib.Algebra.Field.Basic
and_false in Init.SimpLemmas
and_true in Init.SimpLemmas
div_lt_div_of_pos_right in Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
false_and in Init.SimpLemmas
false_or in Init.SimpLemmas
ite_false in Init.SimpLemmas
ite_prop_iff_or in Mathlib.Logic.Basic
ite_true in Init.SimpLemmas
lt_of_lt_of_le in Mathlib.Order.Defs.PartialOrder
lt_trans in Mathlib.Order.Defs.PartialOrder
ne_of_lt in Mathlib.Order.Defs.PartialOrder
neg_add in Mathlib.Algebra.Group.Basic
neg_div in Mathlib.Algebra.Ring.Basic
neg_neg in Mathlib.Algebra.Group.Defs
not_lt in Mathlib.Order.Defs.LinearOrder
or_false in Init.SimpLemmas
sub_eq_add_neg in Mathlib.Algebra.Group.Defs
sub_neg_eq_add in Mathlib.Algebra.Group.Basic
true_and in Init.SimpLemmas
two_pos in Mathlib.Algebra.Order.Monoid.NatCast
</lib_lemmas>

<repo_lemmas>
protected theorem mul_def :
    r * r' = (r.toZMod.val * r'.toZMod.val / RAY_SCALE  : UInt128)

theorem mul_def :
    w₁ * w₂ = ⟨Ray.mul w₁.1 w₂.1, Bool.toSierraBool (Bool.xor (SierraBool.toBool w₁.2) (SierraBool.toBool w₂.2))⟩

theorem ZMod.valMinAbs_add_of_four_lt [NeZero m] {a b : ZMod m}
    (ha : 4 * a.valMinAbs.natAbs < m) (hb : 4 * b.valMinAbs.natAbs < m) :
    (a + b).valMinAbs = a.valMinAbs + b.valMinAbs

theorem ZMod.valMinAbs_add_of_two_lt [NeZero m] {a b : ZMod m}
    (h : 2 * (a.valMinAbs.natAbs + b.valMinAbs.natAbs) < m) :
    (a + b).valMinAbs = a.valMinAbs + b.valMinAbs

theorem ZMod.valMinAbs_cast_of_lt_half [NeZero m] (hm : 2 * m < n) (a : ZMod m) :
  (a.cast : ZMod n).valMinAbs = a.val

protected theorem mul_def :
    w * w' = (w.toZMod.val * w'.toZMod.val / WAD_SCALE  : UInt128)

protected theorem div_def :
    r / r' = (r.toZMod.val * RAY_SCALE / r'.toZMod.val : UInt128)

theorem mul_def :
    w₁ * w₂ = ⟨Wad.mul (w₁.1 : Wad) (w₂.1 : Wad), Bool.toSierraBool (Bool.xor (SierraBool.toBool w₁.2) (SierraBool.toBool w₂.2))⟩

theorem ZMod.val_cast_lt [NeZero m] (n : ℕ) [NeZero n] (a : ZMod m) : (a.cast : ZMod n).val < m

protected theorem div_def :
    w / w' = (w.toZMod.val * WAD_SCALE / w'.toZMod.val : UInt128)

theorem div_def :
    w₁ / w₂ = ⟨Ray.div (w₁.1 : Ray) (w₂.1 : Ray), Bool.toSierraBool (Bool.xor (SierraBool.toBool w₁.2) (SierraBool.toBool w₂.2))⟩

@[simp]
theorem Option.get!_none [Inhabited α] : (.none : Option α).get! = default

@[simp]
theorem Option.get!_some [Inhabited α] (a : α) : (Option.some a).get! = a

theorem div_def :
    w₁ / w₂ = ⟨Wad.div (w₁.1 : Wad) (w₂.1 : Wad), Bool.toSierraBool (Bool.xor (SierraBool.toBool w₁.2) (SierraBool.toBool w₂.2))⟩
</repo_lemmas>

<local_ctx>
import WadrayVerification.Aux

import WadrayVerification.Wadray

open Sierra

aegis_spec "wadray::wadray_signed::SignedWadZeroable::zero" :=
  fun _ (ρ : SignedWad) =>
  ρ = 0

aegis_prove "wadray::wadray_signed::SignedWadZeroable::zero" :=
  fun _ (ρ : SignedWad) => by
  rintro rfl
  rfl

aegis_spec "wadray::wadray_signed::SignedRayZeroable::zero" :=
  fun _ (ρ : SignedRay) =>
  ρ = 0

aegis_prove "wadray::wadray_signed::SignedRayZeroable::zero" :=
  fun _ (ρ : SignedRay) => by
  rintro rfl
  rfl

aegis_spec "wadray::wadray_signed::SignedWadOneable::one" :=
  fun _ (ρ : SignedWad) =>
  ρ = 1

aegis_prove "wadray::wadray_signed::SignedWadOneable::one" :=
  fun _ (ρ : SignedWad) => by
  rintro rfl
  rfl

aegis_spec "wadray::wadray_signed::SignedRayOneable::one" :=
  fun _ (ρ : SignedRay) =>
  ρ = 1

aegis_prove "wadray::wadray_signed::SignedRayOneable::one" :=
  fun _ (ρ : SignedRay) => by
  rintro rfl
  rfl

aegis_spec "wadray::wadray_signed::SignedWadPartialEq::eq" :=
  fun _ (a b : SignedWad) ρ =>
  ρ = Bool.toSierraBool (a.toRat = b.toRat)

aegis_prove "wadray::wadray_signed::SignedWadPartialEq::eq" :=
  fun _ (a b : SignedWad) ρ => by
  unfold «spec_wadray::wadray_signed::SignedWadPartialEq::eq»
  rename_i x
  intro h_auto
  aesop (add safe forward [SignedWad.val_eq_of_toRat_eq, SignedWad.val_eq_zero_of_toRat_neg,
    SignedWad.val_eq_zero_of_toRat_neg'])

aegis_spec "wadray::wadray_signed::SignedRayPartialEq::eq" :=
  fun _ (a b : SignedRay) ρ =>
  ρ = Bool.toSierraBool (a.toRat = b.toRat)

aegis_prove "wadray::wadray_signed::SignedRayPartialEq::eq" :=
  fun _ (a b : SignedRay) ρ => by
  unfold «spec_wadray::wadray_signed::SignedRayPartialEq::eq»
  rename_i x
  intro h_auto
  aesop (add safe forward [SignedRay.val_eq_of_toRat_eq, SignedRay.val_eq_zero_of_toRat_neg,
    SignedRay.val_eq_zero_of_toRat_neg'])

aegis_spec "wadray::wadray_signed::SignedWadPartialEq::ne" :=
  fun _ (a b : SignedWad) ρ =>
  ρ = Bool.toSierraBool (a.toRat ≠ b.toRat)

aegis_prove "wadray::wadray_signed::SignedWadPartialEq::ne" :=
  fun _ (a b : SignedWad) ρ => by
  unfold «spec_wadray::wadray_signed::SignedWadPartialEq::ne»
  rintro rfl
  simp

aegis_spec "wadray::wadray_signed::SignedRayPartialEq::ne" :=
  fun _ (a b : SignedRay) ρ =>
  ρ = Bool.toSierraBool (a.toRat ≠ b.toRat)

aegis_prove "wadray::wadray_signed::SignedRayPartialEq::ne" :=
  fun _ (a b : SignedRay) ρ => by
  unfold «spec_wadray::wadray_signed::SignedRayPartialEq::ne»
  rintro rfl
  simp

aegis_spec "wadray::wadray_signed::SignedWadSigned::is_positive" :=
  fun _ _ (a : SignedWad) _ ρ =>
  ρ = Bool.toSierraBool (a.toRat > 0)

aegis_prove "wadray::wadray_signed::SignedWadSigned::is_positive" :=
  fun _ _ (a : SignedWad) _ ρ => by
  unfold «spec_wadray::wadray_signed::SignedWadSigned::is_positive»
  rintro ⟨w,s,rfl,(⟨h,rfl⟩|⟨h,rfl⟩)⟩
  · aesop (add simp [SignedWad.toRat, Wad.toRat])
  · rcases s with (s|s)
    · simp_all only [Int.ofNat_eq_coe, CharP.cast_eq_zero, Int.cast_zero, ZMod.val_zero,
        SierraBool_toBool_inl, Bool.not_false, Bool.toSierraBool_true, SignedWad.toRat, Wad.toRat,
        Wad.toZMod, ZMod.natCast_val, ite_false, gt_iff_lt, Bool.toSierraBool_decide_inr']
      rw [lt_div_iff (by norm_num [Wad.WAD_SCALE]), zero_mul]
      apply Ne.lt_of_le _ (ZMod.cast_rat_nonneg _)
      intro he
      rw [eq_comm, ZMod.cast_rat_eq_zero_iff] at he; subst he
      simp at h
    · simp [SignedWad.toRat, Wad.toRat]
      rw [le_div_iff (by norm_num [Wad.WAD_SCALE]), zero_mul]
      apply ZMod.cast_rat_nonneg

aegis_spec "wadray::wadray_signed::SignedRaySigned::is_positive" :=
  fun _ _ (a : SignedRay) _ ρ =>
  ρ = Bool.toSierraBool (a.toRat > 0)

aegis_prove "wadray::wadray_signed::SignedRaySigned::is_positive" :=
  fun _ _ (a : SignedWad) _ ρ => by
  unfold «spec_wadray::wadray_signed::SignedRaySigned::is_positive»
  rintro ⟨w,s,rfl,(⟨h,rfl⟩|⟨h,rfl⟩)⟩
  · aesop (add simp [SignedRay.toRat, Ray.toRat])
  · rcases s with (s|s)
    · simp_all only [Int.ofNat_eq_coe, CharP.cast_eq_zero, Int.cast_zero, ZMod.val_zero,
        SierraBool_toBool_inl, Bool.not_false, Bool.toSierraBool_true, SignedRay.toRat, Ray.toRat,
        Ray.toZMod, ZMod.natCast_val, ite_false, gt_iff_lt, Bool.toSierraBool_decide_inr']
      rw [lt_div_iff (by norm_num [Ray.RAY_SCALE]), zero_mul]
      apply Ne.lt_of_le _ (ZMod.cast_rat_nonneg _)
      intro he
      rw [eq_comm, ZMod.cast_rat_eq_zero_iff] at he; subst he
      simp at h
    · simp [SignedRay.toRat, Ray.toRat]
      rw [le_div_iff (by norm_num [Ray.RAY_SCALE]), zero_mul]
      apply ZMod.cast_rat_nonneg

aegis_spec "wadray::wadray_signed::SignedWadSigned::is_negative" :=
  fun _ _ (a : SignedWad) _ ρ =>
  ρ = Bool.toSierraBool (a.toRat < 0)

aegis_prove "wadray::wadray_signed::SignedWadSigned::is_negative" :=
  fun _ _ (a : SignedWad) _ ρ => by
  unfold «spec_wadray::wadray_signed::SignedWadSigned::is_negative»
  rintro ⟨w,s,rfl,(⟨h,rfl⟩|⟨h,rfl⟩)⟩
  · aesop (add simp [SignedWad.toRat, Wad.toRat])
  · have : 0 < (Wad.WAD_SCALE : ℚ) := by norm_num [Wad.WAD_SCALE]
    rcases s with (s|s)
    <;> aesop (add simp [SignedWad.toRat, Wad.toRat, lt_div_iff, le_div_iff,
      Wad.toZMod, ZMod.cast_rat_nonneg], safe apply [Ne.lt_of_le])

aegis_spec "wadray::wadray_signed::SignedRaySigned::is_negative" :=
  fun _ _ (a : SignedRay) _ ρ =>
  ρ = Bool.toSierraBool (a.toRat < 0)

aegis_prove "wadray::wadray_signed::SignedRaySigned::is_negative" :=
  fun _ _ (a : SignedRay) _ ρ => by
  unfold «spec_wadray::wadray_signed::SignedRaySigned::is_negative»
  rintro ⟨w,s,rfl,(⟨h,rfl⟩|⟨h,rfl⟩)⟩
  · aesop (add simp [SignedRay.toRat, Ray.toRat])
  · have : 0 < (Ray.RAY_SCALE : ℚ) := by norm_num [Ray.RAY_SCALE]
    rcases s with (s|s)
    <;> aesop (add simp [SignedRay.toRat, Ray.toRat, lt_div_iff, le_div_iff,
      Ray.toZMod, ZMod.cast_rat_nonneg], safe apply [Ne.lt_of_le])

aegis_spec "wadray::wadray_signed::SignedWadZeroable::is_zero" :=
  fun _ (a : SignedWad) ρ =>
  ρ = Bool.toSierraBool (a.toRat = 0)

aegis_prove "wadray::wadray_signed::SignedWadZeroable::is_zero" :=
  fun _ (a : SignedWad) ρ => by
  unfold «spec_wadray::wadray_signed::SignedWadZeroable::is_zero»
  have : ¬ (Wad.WAD_SCALE = 0) := by
    norm_num [Wad.WAD_SCALE]
  aesop (add simp [SignedWad.toRat, Wad.toRat])

aegis_spec "wadray::wadray_signed::SignedRayZeroable::is_zero" :=
  fun _ (a : SignedRay) ρ =>
  ρ = Bool.toSierraBool (a.toRat = 0)

aegis_prove "wadray::wadray_signed::SignedRayZeroable::is_zero" :=
  fun _ (a : SignedRay) ρ => by
  unfold «spec_wadray::wadray_signed::SignedRayZeroable::is_zero»
  have : ¬ (Ray.RAY_SCALE = 0) := by
    norm_num [Ray.RAY_SCALE]
  aesop (add simp [SignedRay.toRat, Ray.toRat])

aegis_spec "wadray::wadray_signed::SignedWadZeroable::is_non_zero" :=
  fun _ (a : SignedWad) ρ =>
  ρ = Bool.toSierraBool (a.toRat ≠ 0)

aegis_prove "wadray::wadray_signed::SignedWadZeroable::is_non_zero" :=
  fun _ (a : SignedWad) ρ => by
  unfold «spec_wadray::wadray_signed::SignedWadZeroable::is_non_zero»
  aesop (add simp [SignedWad.toRat, Wad.toRat, Wad.toZMod])

aegis_spec "wadray::wadray_signed::SignedRayZeroable::is_non_zero" :=
  fun _ (a : SignedRay) ρ =>
  ρ = Bool.toSierraBool (a.toRat ≠ 0)

aegis_prove "wadray::wadray_signed::SignedRayZeroable::is_non_zero" :=
  fun _ (a : SignedRay) ρ => by
  unfold «spec_wadray::wadray_signed::SignedRayZeroable::is_non_zero»
  aesop (add simp [SignedRay.toRat, Ray.toRat, Ray.toZMod])

aegis_spec "wadray::wadray_signed::SignedWadOneable::is_one" :=
  fun _ (a : SignedWad) ρ =>
  ρ = Bool.toSierraBool (a.toRat = 1)

aegis_prove "wadray::wadray_signed::SignedWadOneable::is_one" :=
  fun _ (a : SignedWad) ρ => by
  unfold «spec_wadray::wadray_signed::SignedWadOneable::is_one»
  rintro ⟨w,s,h⟩
  have : 1000000000000000000 = ((1000000000000000000 : Sierra.UInt128).cast : ℚ) := by
    rw [ZMod.cast_eq_val]; aesop
  have : (1000000000000000000 : ℚ) ≠ 0 := by
    norm_num
  have : ¬ (-(w.cast : ℚ) = 1000000000000000000) := by
    apply ne_of_lt (lt_of_le_of_lt (b := 0) _ (by norm_num))
    simp only [Left.neg_nonpos_iff, ZMod.cast_rat_nonneg]
  aesop (add simp [SignedWad.toRat, Wad.toRat, Wad.toZMod, Wad.WAD_SCALE,
    div_eq_iff, neg_div'], safe forward [ZMod.cast_rat_injective])

aegis_spec "wadray::wadray_signed::SignedRayOneable::is_one" :=
  fun _ (a : SignedRay) ρ =>
  ρ = Bool.toSierraBool (a.toRat = 1)

aegis_prove "wadray::wadray_signed::SignedRayOneable::is_one" :=
  fun _ (a : SignedWad) ρ => by
  unfold «spec_wadray::wadray_signed::SignedRayOneable::is_one»
  rintro ⟨w,s,h⟩
  have : 1000000000000000000000000000 = ((1000000000000000000000000000 : Sierra.UInt128).cast : ℚ) := by
    rw [ZMod.cast_eq_val]; aesop
  have : (1000000000000000000000000000 : ℚ) ≠ 0 := by
    norm_num
  have : ¬ (-(w.cast : ℚ) = 1000000000000000000000000000) := by
    apply ne_of_lt (lt_of_le_of_lt (b := 0) _ (by norm_num))
    simp only [Left.neg_nonpos_iff, ZMod.cast_rat_nonneg]
  aesop (add simp [SignedRay.toRat, Ray.toRat, Ray.toZMod, Ray.RAY_SCALE,
    div_eq_iff, neg_div'], safe forward [ZMod.cast_rat_injective])

aegis_spec "wadray::wadray_signed::SignedWadOneable::is_non_one" :=
  fun _ (a : SignedWad) ρ =>
  ρ = Bool.toSierraBool (a.toRat ≠ 1)

aegis_prove "wadray::wadray_signed::SignedWadOneable::is_non_one" :=
  fun _ (a : SignedWad) ρ => by
  unfold «spec_wadray::wadray_signed::SignedWadOneable::is_non_one»
  rintro ⟨w,s,rfl,h⟩
  have : ¬ (-(w.cast : ℚ) = 1000000000000000000) := by
    apply ne_of_lt (lt_of_le_of_lt (b := 0) _ (by norm_num))
    simp only [Left.neg_nonpos_iff, ZMod.cast_rat_nonneg]
  have : ¬w = 1000000000000000000 → ¬(w.cast : ℚ) = 1000000000000000000 := by
    have hn : 1000000000000000000 = ((1000000000000000000 : Sierra.UInt128).cast : ℚ) := by
      rw [ZMod.cast_eq_val]; aesop
    intros he hee; rw [hn] at hee; have := ZMod.cast_rat_injective hee; contradiction
  aesop (add simp [SignedWad.toRat, Wad.toRat, Wad.toZMod, Wad.WAD_SCALE,
    div_eq_iff, neg_div'], safe forward [ZMod.cast_rat_injective])

aegis_spec "wadray::wadray_signed::SignedRayOneable::is_non_one" :=
  fun _ (a : SignedRay) ρ =>
  ρ = Bool.toSierraBool (a.toRat ≠ 1)

aegis_prove "wadray::wadray_signed::SignedRayOneable::is_non_one" :=
  fun _ (a : SignedRay) ρ => by
  unfold «spec_wadray::wadray_signed::SignedRayOneable::is_non_one»
  rintro ⟨w,s,rfl,h⟩
  have : ¬ (-(w.cast : ℚ) = 1000000000000000000000000000) := by
    apply ne_of_lt (lt_of_le_of_lt (b := 0) _ (by norm_num))
    simp only [Left.neg_nonpos_iff, ZMod.cast_rat_nonneg]
  have : ¬w = 1000000000000000000000000000 → ¬(w.cast : ℚ) = 1000000000000000000000000000 := by
    have hn : 1000000000000000000000000000 = ((1000000000000000000000000000 : Sierra.UInt128).cast : ℚ) := by
      rw [ZMod.cast_eq_val]; aesop
    intros he hee; rw [hn] at hee; have := ZMod.cast_rat_injective hee; contradiction
  aesop (add simp [SignedRay.toRat, Ray.toRat, Ray.toZMod, Ray.RAY_SCALE,
    div_eq_iff, neg_div'], safe forward [ZMod.cast_rat_injective])

aegis_spec "wadray::wadray_signed::BoundedSignedWad::max" :=
  fun _ ρ =>
  ρ = ((U128_MOD - 1 : UInt128), .inl ())

aegis_prove "wadray::wadray_signed::BoundedSignedWad::max" :=
  fun _ ρ => by
  rintro rfl
  rfl
aegis_spec "wadray::wadray_signed::BoundedSignedRay::max" :=
  fun _ ρ =>
  ρ = ((U128_MOD - 1 : UInt128), .inl ())

aegis_prove "wadray::wadray_signed::BoundedSignedRay::max" :=
  fun _ ρ => by
  rintro rfl
  rfl

aegis_spec "wadray::wadray_signed::BoundedSignedWad::min" :=
  fun _ ρ =>
  ρ = ((U128_MOD - 1 : UInt128), .inr ())

aegis_prove "wadray::wadray_signed::BoundedSignedWad::min" :=
  fun _ ρ => by
  rintro rfl
  rfl

aegis_spec "wadray::wadray_signed::BoundedSignedRay::min" :=
  fun _ ρ =>
  ρ = ((U128_MOD - 1 : UInt128), .inr ())

aegis_prove "wadray::wadray_signed::BoundedSignedRay::min" :=
  fun _ ρ => by
  rintro rfl
  rfl

aegis_spec "wadray::wadray_signed::SignedWadPartialOrd::gt" :=
  fun _ _ (a b : SignedWad) _ ρ =>
  ρ = Bool.toSierraBool (b.toRat < a.toRat)

aegis_prove "wadray::wadray_signed::SignedWadPartialOrd::gt" :=
  fun _ _ (a b : SignedWad) _ ρ => by
  unfold «spec_wadray::wadray_signed::SignedWadPartialOrd::gt»
  have : 0 < (Wad.WAD_SCALE : ℚ) := by
    norm_num [Wad.WAD_SCALE]
  rintro ⟨w₁,s₁,w₂,s₂,u₁,u₂,u₃,u₄,u₅,u₆,rfl,rfl,(h|h)⟩
    <;> (cases u₁; cases u₂; cases u₃; cases u₄; cases u₅; cases u₆)
  · rcases h with ⟨rfl,(h|h)⟩
    · rcases h with ⟨rfl,(⟨hne,h⟩|⟨rfl,rfl,rfl⟩)⟩
      · rcases h with (⟨hle,rfl⟩|⟨hlt,rfl⟩)
        · simp [SignedWad.toRat_le_toRat_of_val_le_val_inl hle]
        · simp only [SierraBool_toBool_inr, SierraBool_toBool_inl, Bool.xor_false,
            Bool.toSierraBool_true, Bool.toSierraBool_decide_inr']
          apply lt_of_le_of_ne
          · apply SignedWad.toRat_le_toRat_of_val_le_val_inl
            simp [Wad.toZMod, le_of_lt hlt]
          · intro he
            exact hne (SignedWad.val_eq_of_toRat_eq _ _ he).symm
      · simp only [lt_self_iff_false, decide_False, Bool.toSierraBool_false]
    · rcases h with ⟨rfl,(⟨hne,rfl,rfl⟩|h)⟩
      · simp only [SierraBool_toBool_inl, Bool.not_false, Bool.toSierraBool_true,
          Bool.toSierraBool_decide_inr']
        apply lt_of_le_of_ne
        · simp [SignedWad.toRat_inr_le_toRat_inl]
        · intro he
          exact hne (SignedWad.val_eq_of_toRat_eq _ _ he).symm
      · rcases h with ⟨rfl,(⟨h,rfl,rfl⟩|⟨h,rfl,rfl⟩)⟩
        · simp only [Nat.cast_pos, Bool.toSierraBool_decide_inl', SierraBool_toBool_inl,
            Bool.not_false, Bool.toSierraBool_true, Bool.toSierraBool_decide_inr'] at *
          apply lt_of_lt_of_le (b := 0)
          · apply lt_of_le_of_ne
            · simp [SignedWad.toRat, Wad.toRat_nonneg]
            · simpa [SignedWad.toRat]
          · simp [SignedWad.toRat, Wad.toRat_nonneg]
        · simp only [Nat.cast_pos, SignedWad.toRat, SierraBool_toBool_inl, ite_false,
            Bool.toSierraBool_decide_inr', SierraBool_toBool_inr, ite_true, neg_lt_self_iff,
            Bool.toSierraBool_decide_inl', not_lt] at *
          apply le_of_eq h
  · rcases h with ⟨rfl,(h|h)⟩
    · rcases h with ⟨h',(h|⟨rfl,rfl,rfl⟩)⟩ <;> rcases s₂ with (_|s₂); · simp at h'
      · simp at h'
        rcases h with ⟨hne,(⟨hle,rfl⟩|⟨h,rfl⟩)⟩
        · simp at *
          · cases s₂
            apply lt_of_le_of_ne
            · apply SignedWad.toRat_le_toRat_of_val_ge_val_inr hle
            · intro he
              exact hne (SignedWad.val_eq_of_toRat_eq _ _ he).symm
        · simp at *
          apply SignedWad.toRat_le_toRat_of_val_ge_val_inr (le_of_lt h)
      · simp at *
      · simp at *
    · rcases h with ⟨h',h⟩
      rcases s₂ with (s₂|s₂) <;> cases s₂
      · rcases h with (⟨_,rfl,rfl⟩|⟨rfl,(⟨_,rfl,rfl⟩|⟨_,rfl,rfl⟩)⟩)
          <;> simp [SignedWad.toRat_inr_le_toRat_inl]
      · simp at h'

aegis_spec "wadray::wadray_signed::SignedWadPartialOrd::lt" :=
  fun _ _ (a b : SignedWad) _ ρ =>
  ρ = Bool.toSierraBool (a.toRat < b.toRat)

aegis_prove "wadray::wadray_signed::SignedWadPartialOrd::lt" :=
  fun _ _ (a b : SignedWad) _ ρ => by
  unfold «spec_wadray::wadray_signed::SignedWadPartialOrd::lt»
  have : 0 < (Wad.WAD_SCALE : ℚ) := by
    norm_num [Wad.WAD_SCALE]
  rintro ⟨w₁,s₁,w₂,s₂,u₁,u₂,u₃,u₄,u₅,u₆,rfl,rfl,(h|h)⟩
    <;> (cases u₁; cases u₂; cases u₃; cases u₄; cases u₅; cases u₆)
  · rcases h with ⟨rfl,(h|h)⟩
    · rcases h with ⟨rfl,(⟨hne,h⟩|⟨rfl,rfl,rfl⟩)⟩
      · rcases h with (⟨hle,rfl⟩|⟨hlt,rfl⟩)
        · simp [SignedWad.toRat_le_toRat_of_val_le_val_inl hle]
        · simp only [SierraBool_toBool_inr, SierraBool_toBool_inl, Bool.xor_false,
            Bool.toSierraBool_true, Bool.toSierraBool_decide_inr']
          apply lt_of_le_of_ne
          · apply SignedWad.toRat_le_toRat_of_val_le_val_inl
            simp [Wad.toZMod, le_of_lt hlt]
          · intro he
            exact hne (SignedWad.val_eq_of_toRat_eq _ _ he)
      · simp only [lt_self_iff_false, decide_False, Bool.toSierraBool_false]
    · rcases h with ⟨rfl,(⟨_,rfl,rfl⟩|⟨rfl,(⟨_,rfl,rfl⟩|⟨_,rfl,rfl⟩)⟩)⟩
        <;> simp [SignedWad.toRat_inr_le_toRat_inl]
  · rcases h with ⟨rfl,(h|h)⟩
    · rcases h with ⟨h',(h|⟨rfl,rfl,rfl⟩)⟩ <;> rcases s₂ with (_|s₂); · simp at h'
      · simp at h'
        rcases h with ⟨hne,(⟨hle,rfl⟩|⟨h,rfl⟩)⟩
        · simp at *
          · cases s₂
            apply lt_of_le_of_ne
            · apply SignedWad.toRat_le_toRat_of_val_ge_val_inr hle
            · intro he
              exact hne (SignedWad.val_eq_of_toRat_eq _ _ he)
        · simp at *
          apply SignedWad.toRat_le_toRat_of_val_ge_val_inr (le_of_lt h)
      · simp at *
      · simp at *
    · rcases h with ⟨h',h⟩
      rcases s₂ with (s₂|s₂) <;> cases s₂
      · rcases h with (⟨hne,rfl,rfl⟩|⟨rfl,h⟩)
        · simp
          apply lt_of_le_of_ne
          · apply SignedWad.toRat_inr_le_toRat_inl
          · intro he
            exact hne (SignedWad.val_eq_of_toRat_eq _ _ he)
        · rcases h with (⟨h,rfl,rfl⟩|⟨h,rfl,rfl⟩)
          · simp at *
            apply lt_of_lt_of_le (b := 0)
            · apply lt_of_le_of_ne
              · simp [SignedWad.toRat, Wad.toRat_nonneg]
              · exact h
            · simp [SignedWad.toRat, Wad.toRat_nonneg]
          · simp only [Nat.cast_pos, SierraBool_toBool_inl, Bool.not_false, Bool.toSierraBool_true,
              SignedWad.toRat, SierraBool_toBool_inr, ite_true, neg_eq_zero,
              Bool.toSierraBool_decide_inr', ite_false, neg_lt_self_iff,
              Bool.toSierraBool_decide_inl', not_lt] at *
            simp [h]
      · simp at h'

aegis_spec "wadray::wadray_signed::SignedWadPartialOrd::ge" :=
  fun _ _ (a b : SignedWad) _ ρ =>
  ρ = Bool.toSierraBool (b.toRat ≤ a.toRat)

aegis_prove "wadray::wadray_signed::SignedWadPartialOrd::ge" :=
  fun _ _ (a b : SignedWad) _ ρ => by
  unfold «spec_wadray::wadray_signed::SignedWadPartialOrd::ge»
  rintro rfl
  simp only [← not_lt]
  rw [decide_not]
  simp only [Bool.coe_toSierraBool, Bool.toSierraBool_not]

aegis_spec "wadray::wadray_signed::SignedWadPartialOrd::le" :=
  fun _ _ (a b : SignedWad) _ ρ =>
  ρ = Bool.toSierraBool (a.toRat ≤ b.toRat)

aegis_prove "wadray::wadray_signed::SignedWadPartialOrd::le" :=
  fun _ _ (a b : SignedWad) _ ρ => by
  unfold «spec_wadray::wadray_signed::SignedWadPartialOrd::le»
  rintro rfl
  simp only [← not_lt]
  rw [decide_not]
  simp only [Bool.coe_toSierraBool, Bool.toSierraBool_not]

aegis_spec "wadray::wadray_signed::SignedRayPartialOrd::gt" :=
  fun _ _ (a b : SignedRay) _ ρ =>
  ρ = Bool.toSierraBool (b.toRat < a.toRat)

aegis_prove "wadray::wadray_signed::SignedRayPartialOrd::gt" :=
  fun _ _ (a b : SignedRay) _ ρ => by
  unfold «spec_wadray::wadray_signed::SignedRayPartialOrd::gt»
  have : 0 < (Ray.RAY_SCALE : ℚ) := by
    norm_num [Ray.RAY_SCALE]
  rintro ⟨w₁,s₁,w₂,s₂,u₁,u₂,u₃,u₄,u₅,u₆,rfl,rfl,(h|h)⟩
    <;> (cases u₁; cases u₂; cases u₃; cases u₄; cases u₅; cases u₆)
  · rcases h with ⟨rfl,(h|h)⟩
    · rcases h with ⟨rfl,(⟨hne,h⟩|⟨rfl,rfl,rfl⟩)⟩
      · rcases h with (⟨hle,rfl⟩|⟨hlt,rfl⟩)
        · simp [SignedRay.toRat_le_toRat_of_val_le_val_inl hle]
        · simp only [SierraBool_toBool_inr, SierraBool_toBool_inl, Bool.xor_false,
            Bool.toSierraBool_true, Bool.toSierraBool_decide_inr']
          apply lt_of_le_of_ne
          · apply SignedRay.toRat_le_toRat_of_val_le_val_inl
            simp [Ray.toZMod, le_of_lt hlt]
          · intro he
            exact hne (SignedRay.val_eq_of_toRat_eq _ _ he).symm
      · simp only [lt_self_iff_false, decide_False, Bool.toSierraBool_false]
    · rcases h with ⟨rfl,(⟨hne,rfl,rfl⟩|h)⟩
      · simp only [SierraBool_toBool_inl, Bool.not_false, Bool.toSierraBool_true,
          Bool.toSierraBool_decide_inr']
        apply lt_of_le_of_ne
        · simp [SignedRay.toRat_inr_le_toRat_inl]
        · intro he
          exact hne (SignedRay.val_eq_of_toRat_eq _ _ he).symm
      · rcases h with ⟨rfl,(⟨h,rfl,rfl⟩|⟨h,rfl,rfl⟩)⟩
        · simp only [Nat.cast_pos, Bool.toSierraBool_decide_inl', SierraBool_toBool_inl,
            Bool.not_false, Bool.toSierraBool_true, Bool.toSierraBool_decide_inr'] at *
          apply lt_of_lt_of_le (b := 0)
          · apply lt_of_le_of_ne
            · simp [SignedRay.toRat, Ray.toRat_nonneg]
            · simpa [SignedRay.toRat]
          · simp [SignedRay.toRat, Ray.toRat_nonneg]
        · simp only [Nat.cast_pos, SignedRay.toRat, SierraBool_toBool_inl, ite_false,
            Bool.toSierraBool_decide_inr', SierraBool_toBool_inr, ite_true, neg_lt_self_iff,
            Bool.toSierraBool_decide_inl', not_lt] at *
          apply le_of_eq h
  · rcases h with ⟨rfl,(h|h)⟩
    · rcases h with ⟨h',(h|⟨rfl,rfl,rfl⟩)⟩ <;> rcases s₂ with (_|s₂); · simp at h'
      · simp at h'
        rcases h with ⟨hne,(⟨hle,rfl⟩|⟨h,rfl⟩)⟩
        · simp at *
          · cases s₂
            apply lt_of_le_of_ne
            · apply SignedRay.toRat_le_toRat_of_val_ge_val_inr hle
            · intro he
              exact hne (SignedRay.val_eq_of_toRat_eq _ _ he).symm
        · simp at *
          apply SignedRay.toRat_le_toRat_of_val_ge_val_inr (le_of_lt h)
      · simp at *
      · simp at *
    · rcases h with ⟨h',h⟩
      rcases s₂ with (s₂|s₂) <;> cases s₂
      · rcases h with (⟨_,rfl,rfl⟩|⟨rfl,(⟨_,rfl,rfl⟩|⟨_,rfl,rfl⟩)⟩)
          <;> simp [SignedRay.toRat_inr_le_toRat_inl]
      · simp at h'

aegis_spec "wadray::wadray_signed::SignedRayPartialOrd::lt" :=
  fun _ _ (a b : SignedRay) _ ρ =>
  ρ = Bool.toSierraBool (a.toRat < b.toRat)

aegis_prove "wadray::wadray_signed::SignedRayPartialOrd::lt" :=
  fun _ _ (a b : SignedRay) _ ρ => by
  unfold «spec_wadray::wadray_signed::SignedRayPartialOrd::lt»
  have : 0 < (Ray.RAY_SCALE : ℚ) := by
    norm_num [Ray.RAY_SCALE]
  rintro ⟨w₁,s₁,w₂,s₂,u₁,u₂,u₃,u₄,u₅,u₆,rfl,rfl,(h|h)⟩
    <;> (cases u₁; cases u₂; cases u₃; cases u₄; cases u₅; cases u₆)
  · rcases h with ⟨rfl,(h|h)⟩
    · rcases h with ⟨rfl,(⟨hne,h⟩|⟨rfl,rfl,rfl⟩)⟩
      · rcases h with (⟨hle,rfl⟩|⟨hlt,rfl⟩)
        · simp [SignedRay.toRat_le_toRat_of_val_le_val_inl hle]
        · simp only [SierraBool_toBool_inr, SierraBool_toBool_inl, Bool.xor_false,
            Bool.toSierraBool_true, Bool.toSierraBool_decide_inr']
          apply lt_of_le_of_ne
          · apply SignedRay.toRat_le_toRat_of_val_le_val_inl
            simp [Ray.toZMod, le_of_lt hlt]
          · intro he
            exact hne (SignedRay.val_eq_of_toRat_eq _ _ he)
      · simp only [lt_self_iff_false, decide_False, Bool.toSierraBool_false]
    · rcases h with ⟨rfl,(⟨_,rfl,rfl⟩|⟨rfl,(⟨_,rfl,rfl⟩|⟨_,rfl,rfl⟩)⟩)⟩
        <;> simp [SignedRay.toRat_inr_le_toRat_inl]
  · rcases h with ⟨rfl,(h|h)⟩
    · rcases h with ⟨h',(h|⟨rfl,rfl,rfl⟩)⟩ <;> rcases s₂ with (_|s₂); · simp at h'
      · simp at h'
        rcases h with ⟨hne,(⟨hle,rfl⟩|⟨h,rfl⟩)⟩
        · simp at *
          · cases s₂
            apply lt_of_le_of_ne
            · apply SignedRay.toRat_le_toRat_of_val_ge_val_inr hle
            · intro he
              exact hne (SignedRay.val_eq_of_toRat_eq _ _ he)
        · simp at *
          apply SignedRay.toRat_le_toRat_of_val_ge_val_inr (le_of_lt h)
      · simp at *
      · simp at *
    · rcases h with ⟨h',h⟩
      rcases s₂ with (s₂|s₂) <;> cases s₂
      · rcases h with (⟨hne,rfl,rfl⟩|⟨rfl,h⟩)
        · simp
          apply lt_of_le_of_ne
          · apply SignedRay.toRat_inr_le_toRat_inl
          · intro he
            exact hne (SignedRay.val_eq_of_toRat_eq _ _ he)
        · rcases h with (⟨h,rfl,rfl⟩|⟨h,rfl,rfl⟩)
          · simp at *
            apply lt_of_lt_of_le (b := 0)
            · apply lt_of_le_of_ne
              · simp [SignedRay.toRat, Ray.toRat_nonneg]
              · exact h
            · simp [SignedRay.toRat, Ray.toRat_nonneg]
          · simp only [Nat.cast_pos, SierraBool_toBool_inl, Bool.not_false, Bool.toSierraBool_true,
              SignedRay.toRat, SierraBool_toBool_inr, ite_true, neg_eq_zero,
              Bool.toSierraBool_decide_inr', ite_false, neg_lt_self_iff,
              Bool.toSierraBool_decide_inl', not_lt] at *
            simp [h]
      · simp at h'

aegis_spec "wadray::wadray_signed::SignedRayPartialOrd::ge" :=
  fun _ _ (a b : SignedRay) _ ρ =>
  ρ = Bool.toSierraBool (b.toRat ≤ a.toRat)

aegis_prove "wadray::wadray_signed::SignedRayPartialOrd::ge" :=
  fun _ _ (a b : SignedRay) _ ρ => by
  unfold «spec_wadray::wadray_signed::SignedRayPartialOrd::ge»
  rintro rfl
  simp only [← not_lt]
  rw [decide_not]
  simp only [Bool.coe_toSierraBool, Bool.toSierraBool_not]

aegis_spec "wadray::wadray_signed::SignedRayPartialOrd::le" :=
  fun _ _ (a b : SignedRay) _ ρ =>
  ρ = Bool.toSierraBool (a.toRat ≤ b.toRat)

aegis_prove "wadray::wadray_signed::SignedRayPartialOrd::le" :=
  fun _ _ (a b : SignedRay) _ ρ => by
  unfold «spec_wadray::wadray_signed::SignedRayPartialOrd::le»
  rintro rfl
  simp only [← not_lt]
  rw [decide_not]
  simp only [Bool.coe_toSierraBool, Bool.toSierraBool_not]

aegis_spec "wadray::wadray_signed::SignedWadTryIntoWad::try_into" :=
  fun _ (a : SignedWad) (ρ : Wad ⊕ _) =>
  ρ = if SierraBool.toBool a.2 then .inr () else .inl a.1

aegis_prove "wadray::wadray_signed::SignedWadTryIntoWad::try_into" :=
  fun _ (a : SignedWad) (ρ : Wad ⊕ _) => by
  unfold «spec_wadray::wadray_signed::SignedWadTryIntoWad::try_into»
  aesop

aegis_spec "wadray::wadray_signed::SignedRayTryIntoRay::try_into" :=
  fun _ (a : SignedRay) (ρ : Ray ⊕ _) =>
  ρ = if SierraBool.toBool a.2 then .inr () else .inl a.1

aegis_prove "wadray::wadray_signed::SignedRayTryIntoRay::try_into" :=
  fun _ (a : SignedRay) (ρ : Ray ⊕ _) => by
  unfold «spec_wadray::wadray_signed::SignedRayTryIntoRay::try_into»
  aesop

aegis_spec "wadray::wadray_signed::_felt_sign" :=
  fun _ _ a _ ρ =>
  ρ = Bool.toSierraBool (a.valMinAbs < 0)

aegis_prove "wadray::wadray_signed::_felt_sign" :=
  fun _ _ a _ ρ => by
  unfold «spec_wadray::wadray_signed::_felt_sign»
  rintro ⟨x : UInt256, y : UInt256, h₁, h₂, rfl⟩
  have : (1809251394333065606848661391547535052811553607665798349986546028067936010240 : F).val
          = PRIME / 2 := rfl
  simp only [Int.ofNat_eq_coe, Nat.cast_ofNat, Int.cast_ofNat] at h₂
  simp only [UInt256.val, h₂, h₁, ← not_le (b := a.valMinAbs) (a := 0), ZMod.valMinAbs_nonneg_iff]
  congr; apply propext
  rw [not_le, ← this, ← h₂, UInt256.val, ← h₁, UInt256.val]

aegis_spec "wadray::wadray_signed::_felt_abs" :=
  fun _ _ a _ ρ =>
  ρ = a.valMinAbs.natAbs

aegis_prove "wadray::wadray_signed::_felt_abs" :=
  fun _ _ a _ ρ => by
  unfold «spec_wadray::wadray_signed::_felt_abs»
  sierra_simp'
  rw [← not_le, ZMod.valMinAbs_nonneg_iff, not_le, not_lt, ZMod.natCast_natAbs_valMinAbs a]
  aesop

aegis_spec "wadray::wadray_signed::sign_from_mul" :=
  fun _ a b ρ =>
  ρ = Bool.toSierraBool (xor (SierraBool.toBool a) (SierraBool.toBool b))

aegis_prove "wadray::wadray_signed::sign_from_mul" :=
  fun _ a b ρ => by
  unfold «spec_wadray::wadray_signed::sign_from_mul»
  aesop

aegis_spec "wadray::wadray_signed::signed_wad_from_felt" :=
  fun _ _ a _ (ρ : SignedWad ⊕ _) =>
  if a.valMinAbs.natAbs < U128_MOD
  then ρ.isLeft ∧ ρ.getLeft?.get!.toRat = a.valMinAbs / Wad.WAD_SCALE
  else ρ.isRight

aegis_prove "wadray::wadray_signed::signed_wad_from_felt" :=
  fun _ _ a _ (ρ : SignedWad ⊕ _) => by
  have hlt : a.valMinAbs.natAbs < PRIME := by
    apply lt_of_le_of_lt (ZMod.natAbs_valMinAbs_le a)
    norm_num [PRIME]
  unfold «spec_wadray::wadray_signed::signed_wad_from_felt»
  rintro ⟨_,_,_,(⟨h₁,rfl⟩|⟨h₁,rfl⟩),(⟨h₂,rfl⟩|⟨h₂,rfl⟩)⟩
  · cases h₂
    rw [ZMod.val_natCast_of_lt hlt] at h₁
    simp only [SignedWad.toRat]
    split_ifs with h₃
    · simp_all only [Option.get!, ZMod.cast_nat_cast_of_lt hlt, Sum.getLeft?_inl,
        Bool.coe_toSierraBool, decide_eq_true_eq, decide_True, Bool.toSierraBool_true, Sum.isLeft_inl,
        Wad.toRat, Wad.toZMod, ZMod.val_natCast, Nat.mod_eq_of_lt h₁, neg_div', true_and]
      congr
      rw [Nat.cast_natAbs, Int.cast_abs, neg_eq_iff_eq_neg]
      simp only [abs_eq_neg_self, Int.cast_nonpos]
      exact le_of_lt h₃
    · simp_all only [Option.get!, Sum.getLeft?_inl, Bool.coe_toSierraBool, decide_eq_true_eq,
        not_lt, Sum.isLeft_inl, Wad.toRat, Wad.toZMod, ZMod.natCast_val, true_and,
        ZMod.cast_nat_cast_of_lt hlt, ZMod.cast_nat_cast_of_lt h₁]
      congr
      rw [Nat.cast_natAbs]
      aesop
  · simp at h₂
  · simp at h₂
  · cases h₂
    rw [ZMod.val_natCast_of_lt hlt, ← not_lt] at h₁
    simp [h₁]

aegis_spec "wadray::wadray_signed::signed_ray_from_felt" :=
  fun _ _ a _ (ρ : SignedRay ⊕ _) =>
  if a.valMinAbs.natAbs < U128_MOD
  then ρ.isLeft ∧ ρ.getLeft?.get!.toRat = a.valMinAbs / Ray.RAY_SCALE
  else ρ.isRight

aegis_prove "wadray::wadray_signed::signed_ray_from_felt" :=
  fun _ _ a _ (ρ : SignedRay ⊕ _) => by
  have hlt : a.valMinAbs.natAbs < PRIME := by
    apply lt_of_le_of_lt (ZMod.natAbs_valMinAbs_le a)
    norm_num [PRIME]
  unfold «spec_wadray::wadray_signed::signed_ray_from_felt»
  rintro ⟨_,_,_,(⟨h₁,rfl⟩|⟨h₁,rfl⟩),(⟨h₂,rfl⟩|⟨h₂,rfl⟩)⟩
  · cases h₂
    rw [ZMod.val_natCast_of_lt hlt] at h₁
    simp only [SignedRay.toRat]
    split_ifs with h₃
    · simp_all only [Option.get!, ZMod.cast_nat_cast_of_lt hlt, Sum.getLeft?_inl,
        Bool.coe_toSierraBool, decide_eq_true_eq, decide_True, Bool.toSierraBool_true, Sum.isLeft_inl,
        Ray.toRat, Ray.toZMod, ZMod.val_natCast, Nat.mod_eq_of_lt h₁, neg_div', true_and]
      congr
      rw [Nat.cast_natAbs, Int.cast_abs, neg_eq_iff_eq_neg]
      simp only [abs_eq_neg_self, Int.cast_nonpos]
      exact le_of_lt h₃
    · simp_all only [Option.get!, Sum.getLeft?_inl, Bool.coe_toSierraBool, decide_eq_true_eq,
        not_lt, Sum.isLeft_inl, Ray.toRat, Ray.toZMod, ZMod.natCast_val, true_and,
        ZMod.cast_nat_cast_of_lt hlt, ZMod.cast_nat_cast_of_lt h₁]
      congr
      rw [Nat.cast_natAbs]
      aesop
  · simp at h₂
  · simp at h₂
  · cases h₂
    rw [ZMod.val_natCast_of_lt hlt, ← not_lt] at h₁
    simp [h₁]

aegis_spec "wadray::wadray_signed::SignedWadIntoFelt252::into" :=
  fun _ (a : SignedWad) ρ =>
  ρ = if SierraBool.toBool a.2 then -a.1.cast else a.1.cast

aegis_prove "wadray::wadray_signed::SignedWadIntoFelt252::into" :=
  fun _ (a : SignedWad) ρ => by
  unfold «spec_wadray::wadray_signed::SignedWadIntoFelt252::into»
  aesop

aegis_spec "wadray::wadray_signed::SignedRayIntoFelt252::into" :=
  fun _ (a : SignedRay) ρ =>
  ρ = if SierraBool.toBool a.2 then -a.1.cast else a.1.cast

aegis_prove "wadray::wadray_signed::SignedRayIntoFelt252::into" :=
  fun _ (a : SignedRay) ρ => by
  unfold «spec_wadray::wadray_signed::SignedRayIntoFelt252::into»
  aesop

aegis_spec "wadray::wadray_signed::SignedWadAdd::add" :=
  fun _ _ (a b : SignedWad) _ (ρ : SignedWad ⊕ _) =>
  if |a.toRat + b.toRat| < U128_MOD / Wad.WAD_SCALE
  then ρ.isLeft ∧ ρ.getLeft?.get!.toRat = a.toRat + b.toRat
  else ρ.isRight
</local_ctx>

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

