diff --git a/Fp/Basic.lean b/Fp/Basic.lean
index 2fde194..db1c4c7 100644
--- a/Fp/Basic.lean
+++ b/Fp/Basic.lean
@@ -644,7 +644,7 @@ theorem isZeroOrSubnorm_of_isNonzeroSubnorm {pf : PackedFloat e s} :
   grind [isNonzeroSubnorm, isZeroOrSubnorm]
 
 
-
+-- TODO: delete 'isNZero',
 @[grind →]
 theorem isZero_of_isNZero {pf : PackedFloat e s} :
     pf.isNZero → pf.isZero := by
@@ -1465,7 +1465,6 @@ instance : Std.IsPartialOrder ExtRat where
   le_trans := by grind [le_trans]
   le_antisymm := by grind [le_antisymm]
 
-
 def isNaN (r : ExtRat) : Bool :=
   r = .NaN
 
@@ -1568,6 +1567,16 @@ instance : LE (PackedFloat exWidth sigWidth) where
 theorem le_def (x y : PackedFloat e s) :
   x.le y = (x ≤ y) := rfl
 
+def lt (x y : PackedFloat e s) : Prop :=
+  x ≤ y ∧ x ≠ y
+
+instance : LT (PackedFloat e s) where
+  lt x y := x.lt y
+
+@[simp]
+theorem lt_def (x y : PackedFloat e s) :
+  x.lt y = (x < y) := rfl
+
 @[simp, grind =]
 theorem minus_zero_le_plus_zero {e s} :
     (PackedFloat.getZero e s true ≤ PackedFloat.getZero e s false) =
@@ -1579,11 +1588,22 @@ theorem plus_zero_not_le_minus_zero :
     ¬ (PackedFloat.getZero e s false ≤ PackedFloat.getZero e s true) := by
   simp [getZero, ← PackedFloat.le_def, PackedFloat.le, PackedFloat.isNaN]
 
-
 instance {x y : PackedFloat e s} : Decidable (x ≤ y) := by
     simp only [← PackedFloat.le_def]
     infer_instance
 
+/--
+The successor is the least *strict* upper bound.
+This is used to show that the ordering on 'PackedFloat' is a discrete ordering,
+with adjacent elements having a gap of at least '2^-s'
+-/
+def IsSuccessor (p q : PackedFloat e s) : Prop :=
+  p < q ∧ (∀ (r : PackedFloat e s), p < r → q ≤ r)
+
+instance {x y : PackedFloat e s} : Decidable (x < y) := by
+  simp only [← PackedFloat.lt_def, PackedFloat.lt]
+  infer_instance
+
 def toNumberRatSig {e s} (pf : PackedFloat e s) : Rat :=
   if pf.isNorm then
     1 + pf.sig.toNat / 2 ^ s
@@ -1769,7 +1789,7 @@ def toExtRat' (pf : PackedFloat e s) : ExtRat :=
   else .Number pf.toNumberRat
 
 
-@[simp]
+@[simp, grind =]
 theorem toExtRat'_eq_Number_of_isNormOrNonzeroSubnorm {pf : PackedFloat e s} (hp : pf.isNormOrNonzeroSubnorm := by grind) :
     pf.toExtRat' =
         .Number pf.toNumberRat := by
@@ -1782,7 +1802,7 @@ theorem toExtRat'_eq_Number_of_isNormOrNonzeroSubnorm {pf : PackedFloat e s} (hp
   simp [toExtRat', hnan, hinf, toNumberRat]
 
 
-@[simp]
+@[simp, grind =]
 theorem toExtRat'_eq_zero_of_isZero (pf : PackedFloat e s) (hp : pf.isZero) :
     pf.toExtRat' = .Number 0 := by
   have hnan : pf.isNaN = false := by
@@ -1792,19 +1812,19 @@ theorem toExtRat'_eq_zero_of_isZero (pf : PackedFloat e s) (hp : pf.isZero) :
   simp only [toExtRat', hnan, hinf, cond_false, ExtRat.Number.injEq]
   grind
 
-@[simp]
+@[simp, grind =]
 theorem toExtRat'_eq_NaN_of_isNaN (pf : PackedFloat e s) (hp : pf.isNaN) :
     pf.toExtRat' = .NaN := by
   simp [toExtRat', hp]
 
-@[simp]
+@[simp, grind =]
 theorem toExtRat'_eq_Infinity_of_isInfinite (pf : PackedFloat e s) (hp : pf.isInfinite) :
     pf.toExtRat' = .Infinity pf.sign := by
   rw [toExtRat', hp]
   grind [not_isNaN_of_isInfinite]
 
 
-@[simp, grind! .]
+@[simp, grind! .] -- aggressive?
 theorem toExtRat'_getInfinity {sign : Bool} (hs : 0 < s := by grind) :
     (PackedFloat.getInfinity e s sign).toExtRat' = .Infinity sign := by
   have : (PackedFloat.getInfinity e s sign).isInfinite = true := by
@@ -2303,6 +2323,7 @@ theorem sig_mkZero (sign : Bool) : (mkZero sign : UnpackedFloat e s).sig = 0#s :
 def isZero (uf : UnpackedFloat e s) : Bool :=
   uf.ex == BitVec.intMin e && uf.sig == 0#s
 
+-- | Why does the 'ex' fit?
 @[bv_normalize]
 def normalize (uf : UnpackedFloat e s) (sign := uf.sign) : UnpackedFloat e s :=
   bif uf.sig == 0#s then
@@ -2320,20 +2341,67 @@ theorem sign_normalize (uf : UnpackedFloat e s) : (normalize uf zsign).sign =
   if uf.sig == 0#s then zsign else uf.sign := by
   grind [normalize, mkZero]
 
+@[simp]
+theorem sig_normalize (uf : UnpackedFloat e s) : (normalize uf zsign).sig =
+  if uf.sig == 0#s then 0#s else uf.sig <<< uf.sig.clz := by
+  grind [normalize, mkZero]
+
+@[simp]
+theorem exp_normalize (uf : UnpackedFloat e s) : (normalize uf zsign).ex =
+  if uf.sig == 0#s then BitVec.intMin e else uf.ex - uf.sig.clz.setWidth _ := by
+  grind [normalize, mkZero]
+
+
 @[bv_normalize]
 def toEUnpackedFloat (uf : UnpackedFloat e s) : EUnpackedFloat e s :=
   .mk .Number uf
 
 def toDyadic (uf : UnpackedFloat e s) : Dyadic :=
   let sig : BitVec (s + 1) := uf.sig.setWidth' (Nat.le.step Nat.le.refl)
-  let sig := bif uf.sign then -sig else sig
-  .ofIntWithPrec sig.toInt ((s - 1 : Nat) - uf.ex.toInt)
+  -- | this can lead to overflow in the case where
+  -- sig = intMin. negating intMin causes overflow, so we need to be careful.
+  .ofIntWithPrec (uf.sign.toSign * sig.toInt) ((s - 1 : Nat) - uf.ex.toInt)
 
 def toRat (uf : UnpackedFloat e s) : Rat :=
   uf.toDyadic.toRat
 
--- TODO: add a toRat', and show that these are equivalent.
 
+def toSigNat (uf : UnpackedFloat e s) : Nat :=
+  let sig : BitVec (s + 1) := uf.sig.setWidth' (Nat.le.step Nat.le.refl)
+  sig.toNat
+
+@[simp]
+theorem toNat_toSigNat_eq (uf : UnpackedFloat e s) :
+    toSigNat uf = uf.sig.toNat := by
+  simp [toSigNat]
+
+@[simp]
+theorem toSigNat_of_sig_eq_zero (uf : UnpackedFloat e s)  (h : uf.sig = 0#s) :
+    uf.toSigNat = 0 := by
+  simp [toSigNat, h]
+
+def toExpInt {e s} (uf : UnpackedFloat e s) : Int :=
+  - ((s - 1 : Nat) - uf.ex.toInt)
+
+def toRat' (uf : UnpackedFloat e s) : Rat :=
+  uf.sign.toSign * uf.toSigNat * (2 : Rat) ^ uf.toExpInt
+
+theorem toInt_setWidth_succ_eq_toNat (x : BitVec w) :
+    (x.setWidth (w + 1)).toInt = x.toNat := by
+  rw [BitVec.toInt_eq_toNat_of_msb]
+  · simp
+  · grind only [= BitVec.msb_eq_getMsbD_zero, = BitVec.getMsbD_setWidth]
+
+theorem toRat_eq_toRat' (uf : UnpackedFloat e s) : uf.toRat = uf.toRat' := by
+  rw [toRat, toRat']
+  rw [UnpackedFloat.toDyadic]
+  rw [Dyadic.toRat_ofIntWithPrec_eq_mul_two_pow]
+  simp only [BitVec.setWidth'_eq]
+  rw [toInt_setWidth_succ_eq_toNat (x := uf.sig)]
+  simp [toExpInt]
+  norm_cast
+
+-- TODO: add a toRat', and show that these are equivalent.
 end UnpackedFloat
 
 namespace EUnpackedFloat
@@ -2611,55 +2679,6 @@ theorem toNumberRatSig_times_toNumberRatExp_lt_two_pow_minNormalExp_of_isNonzero
   · grind only [→ not_isNorm_of_isSubnorm]
 
 
-theorem Rat.zpow_sub_eq_zpow_mul_zpow {b : Rat} (hb : b ≠ 0)
-    (x y: Int) : b ^ (x - y) = b ^ x * b ^ (-y) := by
-  rw [Int.sub_eq_add_neg]
-  rw [Rat.zpow_add hb]
-
-theorem Rat.mul_sub (b x y : Rat) : b * (x - y) = b * x - b * y := by
-  grind only
-
-@[simp, grind .]
-theorem Rat.one_le_two_pow_nat {n : Nat} : 1 ≤ (2 : Rat) ^ n := by
-  induction n with
-  | zero => grind
-  | succ n ih =>
-    rw [Rat.pow_succ]
-    grind
-
-theorem Rat.two_pow_le_two_pow_of_le {x y : Int} (h : x ≤ y) : (2 : Rat) ^ x ≤ (2 : Rat) ^ y := by
-  rw [Rat.le_iff_sub_nonneg]
-  rw [show (2 : Rat) ^ x = (2 : Rat) ^ x * 1 by grind only]
-  rw [show y = x + (y - x) by grind only]
-  rw [Rat.zpow_add (by grind only)]
-  rw [← Rat.mul_sub]
-  have : 1 ≤ (2 : Rat) ^ (y - x) := by
-    have : ∃ (k : Nat), y - x = k := by
-      exact Int.nonneg_def.mp h
-    obtain ⟨k, hk⟩ := this
-    rw [hk]
-    simp
-  grind only [Rat.mul_nonneg, Rat.le_of_lt, Fp.Rat.two_pow_pos]
-
-
-theorem Rat.le_mul_of_one_le_of_le  {x y y' : Rat} (hx1 : 1 ≤ x) (hy : 0 ≤ y) (hy' : y ≤ y')
-    : y ≤ x * y' := by
-  suffices 1 * y ≤ x * y' by grind only
-  apply Rat.mul_le_mul_of_le_of_le_of_nonneg_of_nonneg
-  · grind only
-  · grind only
-  · grind only [Rat.le_of_lt, Fp.Rat.two_pow_pos]
-  · grind only [Rat.le_of_lt, Fp.Rat.two_pow_pos]
-
-
-theorem Rat.le_mul_self_of_le_one_of_nonneg {y} {x : Rat} (hx0 : 0 ≤ x ∧ x ≤ 1) (hy : 0 ≤ y)
-    : x * y ≤ y := by
-  suffices x * y ≤ 1 * y by grind only
-  apply Rat.mul_le_mul_of_le_of_le_of_nonneg_of_nonneg
-  · grind only
-  · grind only
-  · grind only [Rat.le_of_lt, Fp.Rat.two_pow_pos]
-  · grind only [Rat.le_of_lt, Fp.Rat.two_pow_pos]
 
 @[simp, grind .]
 theorem toNumberRatSig_times_toNumberRatExp_le_of_isNorm
@@ -2684,7 +2703,6 @@ theorem toNumberRatSig_times_toNumberRatExp_le_of_isNorm
   · grind only [Rat.le_of_lt, Fp.Rat.two_pow_pos]
   · grind only
 
-
 /--
 write being isNorm in terms of an arithmetic condition.
 -/
@@ -2848,8 +2866,117 @@ info: 'PackedFloat.eq_of_toExtRat'_eq' depends on axioms: [propext, Classical.ch
 -/
 #guard_msgs in #print axioms eq_of_toExtRat'_eq
 
+
+@[grind ., grind =]
+theorem isNaN_iff_toExtRat'_eq_NaN (x : PackedFloat e s) (hs : 0 < s) :
+    x.isNaN ↔ x.toExtRat' = .NaN := by
+  constructor
+  · intros h
+    simp [h]
+  · intros hx
+    induction x using PackedFloat.classification <;> grind
 end PackedFloat
 
+namespace UnpackedFloat
+
+@[simp]
+theorem BitVec.clz_zero (w : Nat) : (0#w : BitVec w).clz = w := by
+  rw [BitVec.clz_eq_iff_eq_zero]
+
+
+@[simp, grind =]
+theorem toNat_clz_lt_iff_ne_zero (x : BitVec w) : x.clz.toNat < w ↔ x ≠ 0#w := by
+  have := BitVec.clz_lt_iff_ne_zero (x := x)
+  by_cases hx : x = 0#w
+  · simp [hx]
+  · simp [hx]
+    have := this.mpr (by grind only)
+    simp [BitVec.lt_def] at this
+    grind only
+
+-- | TODO: move this into a separate 'def', because it does sth important:
+-- it moves the leading 1 of the significand to the front,
+-- so we probably want to buidld theory about it?
+theorem toNat_shiftLeft_clz_eq_toNat (uf : UnpackedFloat e s) :
+    (uf.sig <<< uf.sig.clz.toNat).toNat = uf.sig.toNat <<< uf.sig.clz.toNat := by
+  by_cases hs : s = 0
+  · simp [hs]
+    grind only [= Nat.shiftLeft_eq, = BitVec.toNat_zero_length]
+  · by_cases hsig : uf.sig = 0#s
+    · simp [hsig]
+    · simp only [BitVec.toNat_shiftLeft]
+      apply Nat.mod_eq_of_lt
+      have : uf.sig.toNat < 2 ^ s := by grind
+      have := BitVec.two_pow_sub_clz_le_toNat_of_ne_zero (x := uf.sig) (by grind only) (by grind only)
+      have := BitVec.toNat_lt_two_pow_sub_clz (x := uf.sig) (w := s)
+      have : uf.sig.clz.toNat < s := by
+        grind only [#61b3]
+      rw [Nat.shiftLeft_eq]
+      apply Nat.lt_of_lt_of_le (m := 2 ^ (s - uf.sig.clz.toNat) * (2 ^ uf.sig.clz.toNat))
+      · apply Nat.mul_lt_mul_of_lt_of_le
+        · grind only
+        · apply Nat.pow_le_pow_of_le
+          · grind only
+          · grind only
+        · grind only [usr Nat.pow_pos]
+      · rw [← Nat.pow_add]
+        apply Nat.pow_le_pow_of_le
+        · grind only
+        · grind only
+
+
+theorem two_zpow_mul_two_zpow_neg_eq_one (z : Int) :
+  (2 : Rat) ^ z * (2 : Rat) ^ (-z) = 1 := by
+  rw [← Rat.zpow_add (by decide)]
+  rw [show z + (-z) = 0 by grind]
+  simp
+
+/-
+Use this to simplify exponentiation in Q,
+since grind knows the field axioms,
+and can correctly deduce from this
+that these are multiplicative inverses.
+-/
+theorem two_pow_mul_two_pow_neg_intCast_eq_one (z : Nat) :
+  (2 : Rat) ^ z * (2 : Rat) ^ (-( z : Int)) = 1 := by
+  have := two_zpow_mul_two_zpow_neg_eq_one (z := z)
+  simp at this
+  grind
+
+-- TODO: find a more natural phrasing that
+-- this does not overflow.
+theorem UnpackedFloat.toRat_normalize_eq {uf : UnpackedFloat e s}
+  (hex : -(↑(2 ^ e) / 2) ≤ uf.ex.toInt - ↑uf.sig.clz.toNat) :
+  uf.normalize.toRat = uf.toRat := by
+  simp only [UnpackedFloat.toRat_eq_toRat']
+  simp only [toRat', sign_normalize, beq_iff_eq, ite_self]
+  rw [UnpackedFloat.normalize]
+  by_cases hsig : uf.sig = 0#s
+  · simp [hsig]
+  · simp only [show ¬uf.sig == 0#s by grind, BitVec.shiftLeft_eq', cond_false]
+    simp only [toNat_toSigNat_eq]
+    rw [toNat_shiftLeft_clz_eq_toNat]
+    simp only [toExpInt, BitVec.toInt_sub, BitVec.toInt_setWidth,
+      Int.sub_bmod_bmod]
+
+    have : uf.ex.toInt.bmod (2^e) = uf.ex.toInt := by
+      rw [BitVec.toInt_eq_toNat_bmod]
+      simp
+    have hbmod : (uf.ex.toInt - uf.sig.clz.toNat).bmod (2^e) = uf.ex.toInt - uf.sig.clz.toNat := by
+      rw [Int.bmod_eq_of_le]
+      · grind
+      · grind only [usr BitVec.two_mul_toInt_lt]
+    rw [hbmod]
+    have := BitVec.toNat_lt_two_pow_sub_clz (x := uf.sig) (w := s)
+    rw [Nat.shiftLeft_eq]
+    simp
+    push_cast
+    simp only [Int.neg_sub]
+    simp only [Rat.zpow_sub_eq_zpow_mul_zpow (b := 2) (hb := by decide)]
+    grind only [two_pow_mul_two_pow_neg_intCast_eq_one]
+
+end UnpackedFloat
+
 -- Constants
 
 /-- E5M2 floating point representation of 1.0 -/
diff --git a/Fp/SmtLibSemantics.lean b/Fp/SmtLibSemantics.lean
index 3f11d6a..39f7ca7 100644
--- a/Fp/SmtLibSemantics.lean
+++ b/Fp/SmtLibSemantics.lean
@@ -3,6 +3,7 @@ import Fp.Rounding
 import Fp.UnpackedRound
 import Fp.Utils
 import Lean
+import Fp.Theorems.Packing
 open Lean
 
 
@@ -102,7 +103,7 @@ structure RoundableLower (X : Type) (R : Type) where
   lower : R → X
 
 /-- The default embedding of packed floats into the extended rationals. -/
-instance  : RoundableEmbed (PackedFloat e s) ExtRat where
+instance embedPackedFloatExtRat (e s) : RoundableEmbed (PackedFloat e s) ExtRat where
   embed (x : PackedFloat e s) : ExtRat := x.toExtRat
 
 
@@ -114,6 +115,14 @@ structure RoundableAdjunction (X : Type) (R : Type) extends
   RoundableUpper X R
   where
 
+/--
+This is the main property of a lawful rounding adjunction, which states that the lower and upper approximants
+are correct with respect to the embedding. Specifically, `lower` computes the greatest lower bound and `upper` computes the least upper bound of the embedding of `X` into `R`.
+-/
+class LawfulRoundableAdjunction [LE X] [ExtendedNumber R] (adj : RoundableAdjunction X R) where
+  adjunctionLower : ∀ (r : R) (x : X), adj.embed x ≤ r ↔ x ≤ adj.lower r
+  adjunctionUpper : ∀ (r : R) (x : X), r ≤ adj.embed x ↔ adj.upper r ≤ x
+
 /-- Check if the given rational `r` is *strictly in* the lower half
 of the interval `(embed (lower r), embed (upper r))`. -/
 structure RoundableLowerHalf (X : Type) (R : Type) where
@@ -254,26 +263,71 @@ end Round
 def IsLawfulLower [ExtendedNumber R] [RE : RoundableEmbed X R] (r : R) (lower : X) : Prop :=
   RE.embed lower ≤ r ∧ (∀ (lower' : X), RE.embed lower' ≤ r → RE.embed lower' ≤ RE.embed lower)
 
+@[grind →]
+theorem IsLawfulLower.embed_eq_embed [ExtendedNumber R] [RE : RoundableEmbed X R] [Std.IsPartialOrder R] (r : R) (lower1 lower2 : X) :
+  IsLawfulLower r lower1 → IsLawfulLower r lower2 → RE.embed lower1 = RE.embed lower2 := by
+  intro hl1 hl2
+  cases hl1 with
+  | intro hle1 hglb1 =>
+    cases hl2 with
+    | intro hle2 hglb2 =>
+      have hle12 : RE.embed lower1 ≤ RE.embed lower2 := hglb2 lower1 hle1
+      have hle21 : RE.embed lower2 ≤ RE.embed lower1 := hglb1 lower2 hle2
+      grind
+
+/-- lower is the larger than other lower bounds. -/
+@[grind →]
+theorem le_lower_of_le_of_IsLawfulLower [ExtendedNumber R]  [RE : RoundableEmbed X R] (r : R) (lower lower' : X)
+  (hlawful : IsLawfulLower r lower) (hle : RE.embed lower' ≤ r) :
+      RE.embed lower' ≤ RE.embed lower := by
+    grind [IsLawfulLower]
+
+/-- lower is an lower bound -/
+@[grind →]
+theorem lower_le_of_IsLawfulLower [ExtendedNumber R]  [RE : RoundableEmbed X R] (r : R) (lower : X)
+  (hlawful : IsLawfulLower r lower) :
+      RE.embed lower ≤ r := by grind [IsLawfulLower]
+
+
+@[grind →]
+theorem IsLawfulLower.embed_eq_of_IfLawfulLower [ExtendedNumber R] [RE : RoundableEmbed X R] [Std.IsPartialOrder R] (r : R) (upper1 upper2 : X) :
+  IsLawfulLower r upper1 → IsLawfulLower r upper2 → RE.embed upper1 = RE.embed upper2 := by
+  intro hu1 hu2
+  cases hu1 with
+  | intro hle1 lub1 =>
+    cases hu2 with
+    | intro hle2 lub2 =>
+      grind only [#4bb8, #5630]
+
 open Classical in
 noncomputable def smtLibLower [Inhabited X] [ExtendedNumber R] [RoundableEmbed X R] : RoundableLower X R where
   lower (r : R) : X :=
-    if hp : ∃ (x : X), IsLawfulLower r x then
-      Classical.choose hp
-    else
-      default
+    epsilon (IsLawfulLower r)
+
+
+-- TODO: need to know that IsLawfulLower is functional.
 
 /-- 'upper' is a valid least upper bound for 'r'. -/
 def IsLawfulUpper [ExtendedNumber R] [RE : RoundableEmbed X R] (r : R) (upper : X) : Prop :=
   r ≤ RE.embed upper ∧ (∀ (upper' : X), r ≤ RE.embed upper' → RE.embed upper ≤ RE.embed upper')
 
+
+@[grind →]
+theorem IsLawfulUpper.embed_eq_of_IsLawfulUpper [ExtendedNumber R] [RE : RoundableEmbed X R] [Std.IsPartialOrder R] (r : R) (upper1 upper2 : X) :
+  IsLawfulUpper r upper1 → IsLawfulUpper r upper2 → RE.embed upper1 = RE.embed upper2 := by
+  intro hu1 hu2
+  cases hu1 with
+  | intro hle1 lub1 =>
+    cases hu2 with
+    | intro hle2 lub2 =>
+      have hle12 : RE.embed upper2 ≤ RE.embed upper1 := lub2 upper1 hle1
+      have hle21 : RE.embed upper1 ≤ RE.embed upper2 := lub1 upper2 hle2
+      grind
+
 open Classical in
 noncomputable def smtLibUpper {X R} [Inhabited X] [ExtendedNumber R] [RoundableEmbed X R] : RoundableUpper X R where
   upper (r : R) : X :=
-    if hp : ∃ (x : X), IsLawfulUpper r x then
-      /- Use hilbert epsilon to pick -/
-      Classical.choose hp
-    else
-      default
+    epsilon (IsLawfulUpper r)
 
 /--
 The default SMT-Lib adjunction of packed floats into rationals, written `v_ε,σ(f)`,
@@ -283,26 +337,304 @@ for better computational properties.
 We will show later that the `vlower` and `vupper` defined this way agree
 with the galois adjunction expected.
 -/
-noncomputable def smtLibV [Inhabited X] [ExtendedNumber R] [RoundableEmbed X R] :
+noncomputable def smtLibV [Inhabited X] [ExtendedNumber R] (embed : RoundableEmbed X R) :
     RoundableAdjunction X R where
   embed := RoundableEmbed.embed
   lower := smtLibLower.lower
   upper := smtLibUpper.upper
 
+/-- TODO: is this the right way to deal with this? -/
+theorem smtLiV.embed_toRoundableEmbed_eq [Inhabited X] [ExtendedNumber R] (embed : RoundableEmbed X R) :
+  (smtLibV embed).embed = embed.embed := rfl
+
+/-- TODO: is this the right way to deal with this? -/
+@[simp, grind =]
+theorem smtLiV.lower_toRoundableEmbed_eq [Inhabited X] [ExtendedNumber R] (embed : RoundableEmbed X R) :
+  (smtLibV embed).lower = smtLibLower.lower := rfl
+
+@[simp, grind =]
+theorem smtLiV.upper_toRoundableEmbed_eq [Inhabited X] [ExtendedNumber R] (embed : RoundableEmbed X R) :
+  (smtLibV embed).upper = smtLibUpper.upper := rfl
+
+@[simp, grind =] -- TODO: what should be the simp nf?
+theorem RoundableEmbed_embedPackedFloatExtRat_eq_smtLibV_embed:
+    RoundableEmbed.embed (self := embedPackedFloatExtRat e s) = PackedFloat.toExtRat := rfl
+
+open Classical in
+/--
+If a property 'P' is a functional property, then 'epsilon P'
+will pick the element 'p' which obeys that property.
+-/
+theorem epsilon_eq_of_eq [Nonempty α] (P : α → Prop)
+    (hP : ∀ (a b : α), P a → P b → a = b)
+    {p : α}
+    (hp : P p) :
+    epsilon P = p := by
+  have := epsilon_spec (p := P) ⟨p, hp⟩
+  apply hP <;> assumption
+
+-- open Classical in
+-- theorem epsilon_eq_of_eq_of [Nonempty α] (P : α → Prop) (Q : α → Prop)
+--     (hP : ∀ (a b : α), Q a → Q b → a = b)
+--     {p : α}
+--     (hp : P p)
+--     (hq : Q p)
+--     (hpq : ∀ (a : α), Q a → P a) :
+--     epsilon P = p := by
+--   have := epsilon_spec (p := P) ⟨p, hp⟩
+--   have := epsilon_spec (p := Q) ⟨p, hq⟩
+
+
+
+
+-- theorem isNaN_lower_eq
+
+@[simp, grind .]
+theorem IsLawfulLower_mkInfinity (e s : Nat) (hs : 0 < s) (sign : Bool):
+    IsLawfulLower (ExtRat.Infinity sign) (PackedFloat.getInfinity e s sign) := by
+  constructor
+  · simp
+    -- grind
+    rw [PackedFloat.toExtRat'_getInfinity]
+    grind
+  · intros lower hle
+    simp at hle
+    simp
+    rw [PackedFloat.toExtRat'_getInfinity]
+    grind
+
+theorem IsLawfulLower_infinity_iff (e s : Nat) (hs : 0 < s) {x : PackedFloat e s} :
+    IsLawfulLower (ExtRat.Infinity sign) x ↔ x.isInfinite := by
+  constructor
+  · simp [IsLawfulLower]
+    intros hx hx'
+    specialize hx' (PackedFloat.getInfinity e s sign)
+    simp [hs] at hx'
+    specialize hx' (by grind only)
+    have : x.toExtRat' = ExtRat.Infinity sign := by grind only
+    grind only [= PackedFloat.toExtRat'_eq_NaN_of_isNaN, = PackedFloat.toExtRat'_eq_zero_of_isZero,
+      = PackedFloat.toExtRat'_eq_Number_of_isNormOrNonzeroSubnorm,
+      = PackedFloat.isNormOrNonzeroSubnorm_of_not_NaN_not_Infinite_not_Zero]
+  . intros hx
+    simp [IsLawfulLower]
+    simp [hx, hs]
+    induction x using PackedFloat.classification <;> try grind
+    case zeroCase sign =>
+      have : (PackedFloat.getZero e s sign).isZero = true := by
+        refine PackedFloat.isZero_of_isNZero ?_
+
+
+
+@[simp, grind .]
+theorem IsLawfulUpper_mkInfinity (hs : 0 < s) (sign : Bool) :
+    IsLawfulUpper (ExtRat.Infinity sign) (PackedFloat.getInfinity e s sign) := by
+  constructor
+  · simp
+    -- grind
+    rw [PackedFloat.toExtRat'_getInfinity]
+    grind
+  · intros upper hle
+    simp at hle
+    simp
+    rw [PackedFloat.toExtRat'_getInfinity]
+    grind
+
+@[simp, grind .]
+theorem IsLawfulLower_mkNaN : IsLawfulLower ExtRat.NaN (PackedFloat.getNaN e s) := by
+  constructor
+  simp
+  intros lower hLtNaN
+  simp at hLtNaN
+  simp [hLtNaN]
+
+@[simp, grind .]
+theorem IsLawfulLower_NaN_iff {x : PackedFloat e s} : IsLawfulLower ExtRat.NaN x ↔ x.isNaN := by
+  constructor
+  · intros hx
+    simp [IsLawfulLower] at hx
+    obtain ⟨hx, hx'⟩ := hx
+    have : x.isNaN := by grind only [= PackedFloat.toExtRat'_eq_Infinity_of_isInfinite,
+      = PackedFloat.toExtRat'_eq_zero_of_isZero,
+      = PackedFloat.toExtRat'_eq_Number_of_isNormOrNonzeroSubnorm,
+      = PackedFloat.isNormOrNonzeroSubnorm_of_not_NaN_not_Infinite_not_Zero]
+    grind
+  · intros hnan
+    simp [IsLawfulLower]
+    simp [hnan]
+
+
+@[simp, grind .]
+theorem IsLawfulUpper_mkNaN : IsLawfulUpper ExtRat.NaN (PackedFloat.getNaN e s) := by
+  constructor
+  simp
+  intros upper hNaNLe
+  simp at hNaNLe
+  simp [hNaNLe]
+
+@[simp, grind .]
+theorem IslawfulUpper_mkNumber (pf : PackedFloat e s) : IsLawfulUpper pf.toExtRat' pf := by
+  constructor
+  · simp; grind
+  · simp
+
+@[simp, grind .]
+theorem IsLawfulLower_mkNumber (pf : PackedFloat e s) : IsLawfulLower pf.toExtRat' pf := by
+  constructor
+  · simp; grind
+  · simp
+
+
+theorem lower_eq_of_IsLawfulLower_of_not_isNaN_not_isZero {e s} {r : ExtRat}
+    {x : PackedFloat e s}
+    (hx : IsLawfulLower r x)
+    (hnum : ¬ x.isNaN ∧ ¬ x.isZero):
+    smtLibLower.lower r = x := by
+  simp [smtLibLower]
+  -- generalize hu : Classical.epsilon (fun (x : PackedFloat e s) => IsLawfulLower r x) = u
+  -- have := Classical.epsilon_spec (p := fun (x : PackedFloat e s) => IsLawfulLower r x)
+  induction r
+  case NaN =>
+    simp at hx
+    grind only
+  case Infinity =>
+    simp at hx
+    grind only
+
+
+  · apply IsLawfulLower.functional
+
+    have : (embedPackedFloatExtRat e s).embed x =  (embedPackedFloatExtRat e s).embed x' := by grind only [→
+        lower_le_of_IsLawfulLower,
+      → le_lower_of_le_of_IsLawfulLower]
+    simp at this
+    have : x = x' := by
+      apply PackedFloat.eq_of_toExtRat'_eq
+      · grind
+      · -- by contradiction, if true, then x'.toExtRat' will be NaN,
+        -- which will fuck up the toExtRat'.
+        intros hx
+        simp [hx] at this
+        grind only [= PackedFloat.toExtRat'_eq_Infinity_of_isInfinite,
+          = PackedFloat.toExtRat'_eq_Number_of_isNormOrNonzeroSubnorm,
+          = PackedFloat.isNormOrNonzeroSubnorm_of_not_NaN_not_Infinite_not_Zero]
+      · grind
+      · -- by contradiction. if true, then x'.toExtRat' will be 0,
+        -- whch will fuck up the toExtRat'.
+        sorry
+    sorry
+    subst this
+
+
+
+
+@[grind .]
+theorem embed_smtLibLower_eq_of_IsLawfulLower [Inhabited X] [ExtendedNumber R] [instEmbed : RoundableEmbed X R] [Std.IsPartialOrder R]  (r : R) (lower : X) :
+  IsLawfulLower r lower → instEmbed.embed (smtLibLower.lower r) = instEmbed.embed lower := by
+  intro hl
+  simp [smtLibLower]
+  split
+  case isTrue h =>
+    obtain ⟨x, hlx⟩ := h
+    have : instEmbed.embed x = instEmbed.embed lower := by
+      apply IsLawfulLower.functional r x lower hlx hl
+    grind
+  case isFalse h =>
+    simp at h
+    grind
+
+@[simp, grind .]
+theorem toExtRat'_smtLibLower_eq_toExtRat'_of_IsLawfulLower (r : ExtRat) (lower : PackedFloat e s) :
+    IsLawfulLower r lower → (smtLibLower.lower r : PackedFloat e s).toExtRat' = PackedFloat.toExtRat' lower := by
+  intros h
+  have := embed_smtLibLower_eq_of_IsLawfulLower r lower h
+  simp at this
+  assumption
+
+@[simp]
+theorem isNaN_lower_NaN : (smtLibLower.lower ExtRat.NaN : PackedFloat e s).isNaN = true := sorry
+
+-- TODO: show that toExtRat is injective everywhere away from zero.
+
+/-- Lower returns the input at all points except zero. -/
+theorem lower_eq_of_ne_zero {r : ExtRat} {lower : PackedFloat e s}
+    (hs : 0 < s)
+    (hpfNaN : ¬ lower.isNaN)
+    (h : r = lower.toExtRat) (hr : r ≠ 0) :
+    (smtLibLower.lower r : PackedFloat e s) = lower := by
+  induction lower using PackedFloat.classification
+  case nanCase pf hpf =>
+    grind only -- contradiction
+  case infCase sign =>
+    simp [h]
+    simp [PackedFloat.toExtRat'_getInfinity hs]
+    have := IsLawfulLower_mkInfinity e s hs sign
+    sorry
+  case zeroCase pf =>
+    sorry
+  case numCase pf hpf =>
+    sorry
+
+theorem lower_eq_plus_zero :
+  (smtLibLower.lower (0 : ExtRat) : PackedFloat e s) = PackedFloat.getZero e s false := sorry
+
+theorem upper_eq_minus_zero :
+  (smtLibLower.lower (0 : ExtRat) : PackedFloat e s) = PackedFloat.getZero e s true := sorry
+
+/-- Upper returns the input at all points except zero. -/
+theorem upper_eq_of_ne_zero {r : ExtRat} {upper : PackedFloat e s} (h : r = upper.toExtRat) (hr : r ≠ 0) :
+  (smtLibUpper.upper r : PackedFloat e s) = upper := by sorry
+
+ theorem lower_le (r : ExtRat) :
+  ((smtLibLower.lower r) : PackedFloat e s).toExtRat ≤ r := sorry
+
+theorem le_upper (r : ExtRat) :
+  r ≤ ((smtLibUpper.upper r) : PackedFloat e s).toExtRat := sorry
+
+
+instance (he : 0 < e) (hs : 0 < s) : LawfulRoundableAdjunction (smtLibV (embedPackedFloatExtRat e s)) where
+  adjunctionLower := by
+    intros r p
+    simp [instExtendedRat, ← PackedFloat.le_def,
+      PackedFloat.toExtRat_eq_toExtRat']
+    rw [PackedFloat.toExtRat']
+    induction p using PackedFloat.classification
+    case nanCase n hn =>
+      simp [hn]
+      constructor
+      · intros hr
+        simp at hr
+        -- TODO: extract this out into a separate boi.
+        subst hr
+        -- apply PackedFloat.toExtRat'_eq_NaN_of_isNaN (smtLibLower.lower ExtRat.NaN)
+        sorry
+      · sorry
+    case zeroCase sign =>
+      simp [he, show (e = 0) = False by grind, show (s = 0) = False by grind]
+      constructor
+      · intros h
+        sorry
+      · intros h
+        simp at h
+        sorry
+
+    case infCase sign => sorry
+    case numCase n hnum => sorry
+  adjunctionUpper := sorry
+
 @[simp]
 theorem smtLibV_embed_eq [Inhabited X]
-  [ExtendedNumber R] [RoundableEmbed X R]
-    : (smtLibV (X := X) (R := R)).embed = RoundableEmbed.embed := rfl
+  [ExtendedNumber R] (embed : RoundableEmbed X R)
+    : (smtLibV embed).embed = RoundableEmbed.embed := rfl
 
 @[simp]
 theorem smtLibV_lower_eq [Inhabited X]
-  [ExtendedNumber R] [RoundableEmbed X R]
-    : (smtLibV (X := X) (R := R)).lower = smtLibLower.lower := rfl
+  [ExtendedNumber R] (embed : RoundableEmbed X R)
+    : (smtLibV embed).lower = smtLibLower.lower := rfl
 
 @[simp]
 theorem smtLibV_upper_eq [Inhabited X]
-  [ExtendedNumber R] [RoundableEmbed X R]
-    : (smtLibV (X := X) (R := R)).upper = smtLibUpper.upper := rfl
+  [ExtendedNumber R] (embed : RoundableEmbed X R)
+    : (smtLibV embed).upper = smtLibUpper.upper := rfl
 
 /--
 The SMT-Lib definition of the rounding methods for any choice of rounding adjunction 'v'.
@@ -363,6 +695,30 @@ theorem smtLibRoundMethod.lowerHalf_eq {R : Type} (e s : Nat)
     [ExtendedNumber R] :
   (smtLibRoundMethod e s v ves).lowerHalf = (fun r => ExtendedNumber.smtLibEq (v.embed (v.lower r))  (ves.embed (ves.lower r))) := rfl
 
+/--
+two packed floats are at least this far away, or are equal.
+-/
+theorem PackedFloat.toExtRat_sub_toExtRat_ge_of_le (a b : PackedFloat e s) (hab : a ≤ b)
+    (ha : ¬ a.isNaN ∧ ¬ a.isInfinite)
+    (hb : ¬ b.isNaN ∧ ¬ b.isInfinite):
+    ((2 : Rat) ^ (- (s : Int)) ≤ b.toNumberRat - a.toNumberRat) ∨ (a.toNumberRat = b.toNumberRat) := by
+  by_cases hab' : a.toNumberRat = b.toNumberRat
+  · simp [hab']
+  · -- one of them must be nonzero.
+    -- if both are zero, then toNumberRat will be equal.
+    sorry
+
+/--
+The lowerHalf is true if the rational is closer to the lower approximant than the upper approximant.
+-/
+theorem smtLibRoundMethod.lowerHalf_eq_iff (e s : Nat)
+    (v : RoundableAdjunction (PackedFloat e s) ExtRat)
+    (ves : RoundableAdjunction (PackedFloat e (s + 1)) ExtRat)
+    (r : ExtRat) :
+    (smtLibRoundMethod e s v ves).lowerHalf r ↔ ((r - (v.lower r).toExtRat) ≤ ((v.upper r).toExtRat - r)) := by
+  sorry
+
+
 theorem smtLibRoundMethod.tieBreak_eq {R : Type} (e s : Nat)
     (v : RoundableAdjunction (PackedFloat e s) R)
     (ves : RoundableAdjunction (PackedFloat e (s + 1)) R)
@@ -371,6 +727,15 @@ theorem smtLibRoundMethod.tieBreak_eq {R : Type} (e s : Nat)
     (v.embed (v.lower r) < ves.embed (ves.lower r)) =
     (ves.embed (ves.upper r) < (v.embed (v.upper r)))) := rfl
 
+/--
+The tieBreak is true iff the rational is closer to the upper approximant than the lower approximant.
+-/
+theorem smtLibRoundMethod.tieBreak_eq_iff (e s : Nat)
+    (v : RoundableAdjunction (PackedFloat e s) ExtRat)
+    (ves : RoundableAdjunction (PackedFloat e (s + 1)) ExtRat)
+    (r : ExtRat) :
+  (smtLibRoundMethod e s v ves).tieBreak r ↔ ((r - (v.lower r).toExtRat) = ((v.upper r).toExtRat - r)) := by sorry
+
 instance [hExtended : ExtendedNumber R]
     [DecidableRel hExtended.smtLibEq]
     {v : RoundableAdjunction (PackedFloat e s) R}
@@ -387,6 +752,19 @@ instance [hExtended : ExtendedNumber R]
   rw [smtLibRoundMethod]
   infer_instance
 
+/--
+A successor is the least *strict* upper bound. So, successor gives the next
+packed float.
+Note that this sucks, because this will mean that
+the successor of -0 is not necessarily +0,
+which is probably not what we want.
+Instead, we should build this as PackedFloat theory,
+and show that the ordering on PackedFloat has a 'successor'.
+-/
+def IsLawfulSuccessor [ExtendedNumber R] [RE : RoundableEmbed X R] (r : R) (upper : X) : Prop :=
+  r < RE.embed upper ∧ (∀ (upper' : X), r < RE.embed upper' → RE.embed upper ≤ RE.embed upper')
+
+
 -- end SmtLibRoundMethod
 
 namespace SmtLibFunctions
diff --git a/Fp/Theorems/Packing.lean b/Fp/Theorems/Packing.lean
index c10a783..0ba8f7e 100644
--- a/Fp/Theorems/Packing.lean
+++ b/Fp/Theorems/Packing.lean
@@ -100,15 +100,19 @@ theorem toEUnpackedFloat_not_isInfinite {uf : UnpackedFloat e s}
 theorem toRat_eq {uf : UnpackedFloat e s}
   : uf.toRat = uf.sign.toSign * uf.sig.toNat * 2 ^ (uf.ex.toInt - (s - 1 : Nat)) := by
   have hmsb : (uf.sig.setWidth' _).msb = false := BitVec.msb_setWidth'_of_lt (Nat.lt_succ_self s)
-  simp only [toRat, toDyadic, cond_eq_ite, Dyadic.toRat_ofIntWithPrec_eq_mul_two_pow,
+  simp only [toRat, toDyadic, Dyadic.toRat_ofIntWithPrec_eq_mul_two_pow,
     Int.neg_sub, Bool.toSign]
   congr
   split
   · simp only [Rat.intCast_neg, Rat.intCast_ofNat, ← Rat.intCast_natCast, Rat.neg_mul, Rat.one_mul]
     rewrite [← Rat.intCast_neg]
     congr
-    rewrite [← Int.neg_inj, BitVec.neg_toInt_neg hmsb]
+    simp only [Int.reduceNeg, BitVec.setWidth'_eq, Int.neg_one_mul,
+      Int.neg_inj]
+    rw [BitVec.toInt_eq_msb_cond]
     simp
+    intros hcontra
+    simp [BitVec.msb_eq_getLsbD_last] at hcontra
   · rewrite [BitVec.toInt_eq_toNat_of_msb hmsb]
     simp [Rat.intCast_natCast]
 
@@ -184,7 +188,8 @@ theorem sigWidth_add_bias_le_exponentWidth_sub_one : s + bias e ≤ 2 ^ (exponen
   simp only [bias, exponentWidth]
   grind only [!Nat.two_pow_pos, !Nat.log2_eq_iff, #569066451790c837, #ccfcc644d1be4e5b]
 
--- theorem expWidth_lt_exponentWidth : e < exponentWidth e s := by
+-- theorem expWidth_lt_exponentWidth :
+--   e < exponentWidth e s := by
 --   unfold exponentWidth
 --   induction e with
 --   | zero => simp
@@ -230,7 +235,7 @@ theorem toRat_normalize_eq_toRat {uf : UnpackedFloat e s}
       have hSigClzNeZero' : uf.sig.clz.toNat < s := by
         rw [BitVec.lt_def] at hSigClzNeZero
         simp at hSigClzNeZero
-        apply hSigClzNeZero
+        apply (toNat_clz_lt_iff_ne_zero ..) |>.mpr h
       rw [BitVec.toInt_setWidth]
       have : (uf.sig.clz.toNat : Int).bmod (2 ^ e) = uf.sig.clz.toNat := by
         refine Int.bmod_eq_of_le hle ?_
@@ -372,7 +377,7 @@ theorem exponentWidth_gt_zero : exponentWidth e s > 0 := by
 -- | TODO: refactor by pulling out lemmas that talk about the 'toNat' of the various
 -- significand, and so on.
 theorem toExtRat_unpack_eq_toExtRat {pf : PackedFloat e s}
-  : pf.unpack.toExtRat = pf.toExtRat := by
+    : pf.unpack.toExtRat = pf.toExtRat := by
   simp only [unpack, unpackNormOrNonzeroSubnorm, BitVec.truncate_eq_setWidth, toExtRat_eq_toExtRat']
   cases hNaN : pf.isNaN
   · cases hInf : pf.isInfinite
@@ -480,7 +485,7 @@ theorem toExtRat_unpack_eq_toExtRat {pf : PackedFloat e s}
             Nat.add_one_sub_one, @Int.sub_eq_add_neg _ s, @Rat.zpow_add 2 (by decide)]
           rw [Rat.mul_comm _ (2 ^ (-s : Int)), ← Rat.mul_assoc, Rat.add_mul, ← Rat.zpow_natCast, ← Rat.zpow_add (by decide) s (-s), Int.add_neg_eq_sub, Int.sub_self, Rat.zpow_zero, Rat.zpow_neg, ← Rat.div_def]
       · simp only [EUnpackedFloat.toExtRat, cond_true, cond_false, EUnpackedFloat.mkZero_not_isNaN,
-        EUnpackedFloat.mkZero_not_isInfinite, toExtRat', hNaN, hInf, hZero]
+        EUnpackedFloat.mkZero_not_isInfinite, toExtRat', hNaN, hInf]
         simp [EUnpackedFloat.mkZero]
         simp [hZero]
     · simp only [EUnpackedFloat.toExtRat, cond_true, cond_false,
diff --git a/Fp/Theorems/SmtLibSemanticsQ.lean b/Fp/Theorems/SmtLibSemanticsQ.lean
index be8648b..db8fd6f 100644
--- a/Fp/Theorems/SmtLibSemanticsQ.lean
+++ b/Fp/Theorems/SmtLibSemanticsQ.lean
@@ -14,7 +14,9 @@ into a packed float of 'eout, sout' according to the SMT-Lib semantics.
 Our proofs will be against this definition.
 -/
 noncomputable abbrev smtLibRoundMethodQ (eout sout : Nat) : SmtLibSemantics.RoundMethod (PackedFloat eout sout) ExtRat :=
-  SmtLibSemantics.smtLibRoundMethod eout sout (R := ExtRat) (SmtLibSemantics.smtLibV) (SmtLibSemantics.smtLibV)
+  SmtLibSemantics.smtLibRoundMethod eout sout
+    (SmtLibSemantics.smtLibV (SmtLibSemantics.embedPackedFloatExtRat eout sout))
+    (SmtLibSemantics.smtLibV (SmtLibSemantics.embedPackedFloatExtRat eout (sout + 1)))
 
 end SmtLibSemanticsQ
 
diff --git a/Fp/Theorems/UnpackedRound.lean b/Fp/Theorems/UnpackedRound.lean
index 49f0c58..d71e072 100644
--- a/Fp/Theorems/UnpackedRound.lean
+++ b/Fp/Theorems/UnpackedRound.lean
@@ -6,52 +6,64 @@ import Fp.Theorems.Packing
 
 
 namespace Fp
+open SmtLibSemantics
 
 @[simp]
 theorem roundQ_eq (eout sout : Nat) (rm : RoundingMode) (sign : Bool) (r : ExtRat):
     (Fp.SmtLibSemanticsQ.smtLibRoundMethodQ eout sout).round rm sign r =
     (SmtLibSemantics.smtLibRoundMethod eout sout
-      SmtLibSemantics.smtLibV SmtLibSemantics.smtLibV).round rm sign
+      (SmtLibSemantics.smtLibV (SmtLibSemantics.embedPackedFloatExtRat eout sout))
+      (SmtLibSemantics.smtLibV (SmtLibSemantics.embedPackedFloatExtRat eout (sout + 1)))).round rm sign
     r := rfl
 
 set_option warn.sorry false in
 @[simp]
-theorem lower_NaN_eq_PackedFloat_mkNaN :
-  SmtLibSemantics.smtLibLower.lower ExtRat.NaN = (PackedFloat.getNaN e s : PackedFloat e s) := sorry
+theorem lower_NaN_eq_PackedFloat_getNaN :
+  SmtLibSemantics.smtLibLower.lower ExtRat.NaN = (PackedFloat.getNaN e s) := sorry
 
 set_option warn.sorry false in
 @[simp]
-theorem upper_NaN_eq_PackedFloat_mkNaN :
-  SmtLibSemantics.smtLibUpper.upper ExtRat.NaN = (PackedFloat.getNaN e s : PackedFloat e s) := sorry
+theorem upper_NaN_eq_PackedFloat_getNaN :
+  SmtLibSemantics.smtLibUpper.upper ExtRat.NaN = (PackedFloat.getNaN e s) := sorry
 
 @[simp]
 theorem roundRNA_mkNaN (eout sout : Nat) (sign : Bool) :
-  (SmtLibSemantics.smtLibRoundMethod eout sout SmtLibSemantics.smtLibV SmtLibSemantics.smtLibV).roundRNA sign
+  (SmtLibSemantics.smtLibRoundMethod eout sout
+    (SmtLibSemantics.smtLibV (SmtLibSemantics.embedPackedFloatExtRat eout sout))
+    (SmtLibSemantics.smtLibV (SmtLibSemantics.embedPackedFloatExtRat eout (sout + 1)))).roundRNA sign
     (ExtRat.NaN) = PackedFloat.getNaN eout sout := by
   simp [SmtLibSemantics.RoundMethod.roundRNA]
 
 @[simp]
 theorem roundRNE_mkNaN (eout sout : Nat) (sign : Bool) :
-  (SmtLibSemantics.smtLibRoundMethod eout sout SmtLibSemantics.smtLibV SmtLibSemantics.smtLibV).roundRNE sign
+  (SmtLibSemantics.smtLibRoundMethod eout sout
+    (SmtLibSemantics.smtLibV (SmtLibSemantics.embedPackedFloatExtRat eout sout))
+    (SmtLibSemantics.smtLibV (SmtLibSemantics.embedPackedFloatExtRat eout (sout + 1)))).roundRNE sign
     (ExtRat.NaN) = PackedFloat.getNaN eout sout := by
   simp [SmtLibSemantics.RoundMethod.roundRNE]
 
 @[simp]
 theorem roundRTP_mkNaN (eout sout : Nat) (sign : Bool) :
-  (SmtLibSemantics.smtLibRoundMethod eout sout SmtLibSemantics.smtLibV SmtLibSemantics.smtLibV).roundRTP sign
+  (SmtLibSemantics.smtLibRoundMethod eout sout
+    (SmtLibSemantics.smtLibV (SmtLibSemantics.embedPackedFloatExtRat eout sout))
+    (SmtLibSemantics.smtLibV (SmtLibSemantics.embedPackedFloatExtRat eout (sout + 1)))).roundRTP sign
     (ExtRat.NaN) = PackedFloat.getNaN eout sout := by
   simp [SmtLibSemantics.RoundMethod.roundRTP]
 
 @[simp]
 theorem roundRTN_mkNaN (eout sout : Nat) (sign : Bool) :
-  (SmtLibSemantics.smtLibRoundMethod eout sout SmtLibSemantics.smtLibV SmtLibSemantics.smtLibV).roundRTN sign
+  (SmtLibSemantics.smtLibRoundMethod eout sout
+    (SmtLibSemantics.smtLibV (SmtLibSemantics.embedPackedFloatExtRat eout sout))
+    (SmtLibSemantics.smtLibV (SmtLibSemantics.embedPackedFloatExtRat eout (sout + 1)))).roundRTN sign
     (ExtRat.NaN) = PackedFloat.getNaN eout sout := by
   simp [SmtLibSemantics.RoundMethod.roundRTN]
   rcases sign <;> simp
 
 @[simp]
 theorem rountRTZ_mkNaN (eout sout : Nat) (sign : Bool) :
-  (SmtLibSemantics.smtLibRoundMethod eout sout SmtLibSemantics.smtLibV SmtLibSemantics.smtLibV).roundRTZ sign
+  (SmtLibSemantics.smtLibRoundMethod eout sout
+    (SmtLibSemantics.smtLibV (SmtLibSemantics.embedPackedFloatExtRat eout sout))
+    (SmtLibSemantics.smtLibV (SmtLibSemantics.embedPackedFloatExtRat eout (sout + 1)))).roundRTZ sign
     (ExtRat.NaN) = PackedFloat.getNaN eout sout := by
   simp [SmtLibSemantics.RoundMethod.roundRTZ]
   rcases sign <;> simp
@@ -59,7 +71,9 @@ theorem rountRTZ_mkNaN (eout sout : Nat) (sign : Bool) :
 
 @[simp]
 theorem round_eq_mkNaN_of_NaN {sign} {eout sout : Nat} {rm : RoundingMode} :
-    (SmtLibSemantics.smtLibRoundMethod eout sout SmtLibSemantics.smtLibV SmtLibSemantics.smtLibV).round
+    (SmtLibSemantics.smtLibRoundMethod eout sout
+      (SmtLibSemantics.smtLibV (SmtLibSemantics.embedPackedFloatExtRat eout sout))
+      (SmtLibSemantics.smtLibV (SmtLibSemantics.embedPackedFloatExtRat eout (sout + 1)))).round
         rm sign ExtRat.NaN = PackedFloat.getNaN eout sout := by
   rcases rm
   · simp
@@ -71,14 +85,34 @@ theorem round_eq_mkNaN_of_NaN {sign} {eout sout : Nat} {rm : RoundingMode} :
 set_option warn.sorry false in
 @[simp]
 theorem round_eq_mkZero_of_mkZero {zeroSign : Bool} {eout sout : Nat} {rm : RoundingMode} :
-    (SmtLibSemantics.smtLibRoundMethod eout sout SmtLibSemantics.smtLibV SmtLibSemantics.smtLibV).round
+    (SmtLibSemantics.smtLibRoundMethod eout sout
+      (SmtLibSemantics.smtLibV (SmtLibSemantics.embedPackedFloatExtRat eout sout))
+      (SmtLibSemantics.smtLibV (SmtLibSemantics.embedPackedFloatExtRat eout (sout + 1)))
+    ).round
         rm zeroSign (ExtRat.Number 0) = PackedFloat.getZero eout sout zeroSign := by
   rcases rm <;> sorry
 
+/--
+'uf' approximtes 'r' upto rounding.
+-/
+structure ApproximatesUptoRounding (uf : UnpackedFloat ein sin) (er : ExtRat) (eout sout : Nat) : Prop where
+  /-- we have at least 2 bits more, of guard and sticky. -/
+  hSigGe : sin + 2 ≥ sout
+  /-- we have at least as much exponent range. -/
+  hExpGe : ein ≥ eout -- we have at least as much exponent range
+  /-- rational values have (sout + 1) bits of precision. -/
+  hApproxUptoGuard : ∀ (r : Rat), .Number r = er → (uf.toRat - r).abs < (2 : Rat) ^ (-(sout + 1 : Int))
+  /-- the sticky bit is zero iff the number truncated upto the guard bit equals -/
+  hStickyBitCorrect : ∀ (r : Rat), .Number r = er → ((uf.sig.extractMsb' (sout + 1) (sin - (sout + 1)) ≠ 0) = decide (r = uf.toRat))
+
 set_option warn.sorry false in
-theorem roundQ_Number_eq_round (er : ExtRat) (uf : UnpackedFloat ein sin)
-    (hruf : ExtRat.Number uf.toRat = er) :
-    (SmtLibSemantics.smtLibRoundMethod eout sout SmtLibSemantics.smtLibV SmtLibSemantics.smtLibV).round rm sign
+theorem roundQ_Number_eq_round
+    (er : ExtRat) (uf : UnpackedFloat ein sin)
+    (hruf : ApproximatesUptoRounding uf er eout sout) (rm : RoundingMode) (sign : Bool) :
+    (SmtLibSemantics.smtLibRoundMethod eout sout
+      (SmtLibSemantics.smtLibV (SmtLibSemantics.embedPackedFloatExtRat eout sout))
+      (SmtLibSemantics.smtLibV (SmtLibSemantics.embedPackedFloatExtRat eout (sout + 1)))
+    ).round rm sign
       er =
       (UnpackedFloat.round uf rm).pack := by sorry
 
@@ -97,42 +131,35 @@ theorem roundQ_Number_eq_round (er : ExtRat) (uf : UnpackedFloat ein sin)
 
 @[simp]
 theorem roundQ_eq_round_of_Infinity {zeroSign infSign : Bool} {e s : Nat} {rm : RoundingMode} :
-    (SmtLibSemantics.smtLibRoundMethod e s SmtLibSemantics.smtLibV SmtLibSemantics.smtLibV).round rm zeroSign
+    (SmtLibSemantics.smtLibRoundMethod e s
+      (SmtLibSemantics.smtLibV (SmtLibSemantics.embedPackedFloatExtRat e s))
+      (SmtLibSemantics.smtLibV (SmtLibSemantics.embedPackedFloatExtRat e (s + 1)))
+    ).round rm zeroSign
       (ExtRat.Infinity infSign) =
       PackedFloat.getInfinity e s infSign := by sorry
 
-/--
-Case splitting on the different values a packed float
-can have: it can be nan, infinity, zero, or a nonzero normal/subnormal.+
--/
-@[elab_as_elim]
-theorem PackedFloat.kindCasesNaNInfZeroNum {P : PackedFloat e s → Prop}
-    (x : PackedFloat e s)
-    (nanCase : ∀ (n : PackedFloat e s), n.isNaN → P n)
-    (infCase : ∀ sign, P (PackedFloat.getInfinity e s sign))
-    (zeroCase : ∀ sign, P (PackedFloat.getZero e s sign))
-    (numCase : ∀ (n : PackedFloat e s), n.isNormOrNonzeroSubnorm → P n) :
-    P x := by
-  have := x.classification_exhaustive
-  simp at this
-  by_cases h1 : x.isNaN
-  · grind
-  · by_cases h2 : x.isInfinite
-    · grind
-    · by_cases h3 : x.isZero
-      · grind
-      · by_cases h4 : x.isNonzeroSubnorm
-        · grind
-        · by_cases h5 : x.isNorm
-          · grind
-          · grind
 
 @[grind <=]
 theorem PackedFloat.eq_of_unpack_eq_unpack_of_isInfinity {x y : PackedFloat e s}
     (hs : 0 < s) (he : 0 < e)
     (hx : x.isInfinite) (hy : y.isInfinite) (h : x.unpack = y.unpack) :
     x = y := by
-  cases x using PackedFloat.kindCasesNaNInfZeroNum <;> try grind
+  cases x using PackedFloat.classification <;> try grind
+
+/--
+Purely arithmetic fact that needs to be proven,
+which should just be to show that the fixed point computation equals the
+rational multiplication.
+Actually, this is too strong, the theorem statemtnt should be able to state
+something weaker, that only upto (s+1) bits agree,
+and that the sticky bit is computed correctly.
+-/
+theorem ApproximatesUptoRounding_mul_mul
+  (a b : PackedFloat ein sin)
+  (ha : a.isNormOrNonzeroSubnorm = true)
+  (hb : b.isNormOrNonzeroSubnorm = true) :
+  ApproximatesUptoRounding (a.unpackNormOrNonzeroSubnorm.mul b.unpackNormOrNonzeroSubnorm)
+  (ExtRat.Number a.toNumberRat * ExtRat.Number b.toNumberRat) ein sin := sorry
 
 set_option warn.sorry false in
 /--
@@ -144,7 +171,7 @@ theorem mul_eq_mul {ein sin : Nat} (hsin : 0 < sin) (he : 0 < ein)
     rm a b = PackedFloat.mul rm a b := by
   simp [SmtLibSemantics.SmtLibFunctions.mul]
   rw [PackedFloat.mul, EUnpackedFloat.mul]
-  cases a using PackedFloat.kindCasesNaNInfZeroNum
+  cases a using PackedFloat.classification
   case nanCase hnan =>
     simp [hnan]
     rw [round_eq_mkNaN_of_NaN]
@@ -153,7 +180,7 @@ theorem mul_eq_mul {ein sin : Nat} (hsin : 0 < sin) (he : 0 < ein)
     rw [← ExtRat.mul_def]
     unfold ExtRat.mul
     simp
-    cases b using PackedFloat.kindCasesNaNInfZeroNum
+    cases b using PackedFloat.classification
     case nanCase hb =>
       simp [hb]
       -- | why does this not apply automatically?
@@ -184,7 +211,7 @@ theorem mul_eq_mul {ein sin : Nat} (hsin : 0 < sin) (he : 0 < ein)
       sorry
   case zeroCase sign =>
     simp [he]
-    cases b using PackedFloat.kindCasesNaNInfZeroNum
+    cases b using PackedFloat.classification
     case nanCase hb =>
       simp [hb]
       rw [round_eq_mkNaN_of_NaN]
@@ -211,7 +238,7 @@ theorem mul_eq_mul {ein sin : Nat} (hsin : 0 < sin) (he : 0 < ein)
     rw [PackedFloat.unpack_eq_mkNumber_of_isNormOrNonzeroSubnorm ha]
     rw [PackedFloat.toExtRat'_eq_Number_of_isNormOrNonzeroSubnorm ha]
     -- interesting case, when a is a number.
-    cases b using PackedFloat.kindCasesNaNInfZeroNum
+    cases b using PackedFloat.classification
     case nanCase hb =>
       simp [hb]
       rw [round_eq_mkNaN_of_NaN]
@@ -221,7 +248,9 @@ theorem mul_eq_mul {ein sin : Nat} (hsin : 0 < sin) (he : 0 < ein)
       simp [this]
       rw [← ExtRat.mul_def, ExtRat.mul]
       simp only [SmtLibSemantics.instExtendedRat, SmtLibSemantics.instExtendedRat.eq_1, roundQ_eq]
-      simp [show a.toNumberRat < 0 ↔ a.sign = true by sorry]
+      simp [show a.toNumberRat < 0 ↔ a.sign = true by grind only [→
+          PackedFloat.sign_iff_toNumberRat_neg,
+        #34bd]]
       simp [show a.toNumberRat = 0 ↔ a.isZero by sorry]
       simp [show ¬ a.isZero by grind]
       rw [roundQ_eq_round_of_Infinity]
@@ -237,10 +266,7 @@ theorem mul_eq_mul {ein sin : Nat} (hsin : 0 < sin) (he : 0 < ein)
       simp [this]
       have : ¬ b.isZero := by grind
       simp [this]
-      rw [roundQ_Number_eq_round]
       rw [PackedFloat.toExtRat'_eq_Number_of_isNormOrNonzeroSubnorm hb]
-      simp only [ExtRat.number_mul_number_eq, ExtRat.Number.injEq]
-      -- Purely arithmetic statement.
-      -- ⊢ (a.unpackNormOrNonzeroSubnorm.mul b.unpackNormOrNonzeroSubnorm).toRat = a.toNumberRat * b.toNumberRat
-      sorry
+      apply roundQ_Number_eq_round
+      apply ApproximatesUptoRounding_mul_mul <;> assumption
 end Fp
diff --git a/Fp/UnpackedRound.lean b/Fp/UnpackedRound.lean
index 57fdd74..bad1c01 100644
--- a/Fp/UnpackedRound.lean
+++ b/Fp/UnpackedRound.lean
@@ -4,6 +4,7 @@ import Fp.MulInv
 import Fp.Grind
 import Fp.ForLean.Rat
 import Fp.Rounding
+import Fp.Theorems.Packing
 
 @[bv_normalize]
 def BitVec.leadingOne (w : Nat) : BitVec w :=
@@ -759,6 +760,175 @@ def UnpackedFloat.round {expWidth sigWidth : Nat} {targetExponentWidth targetSig
     (isZero := inUf.isZero)
   result
 
+/--
+The core rounding function,
+that rounds an `UnpackedFloat` to the target exponent and significand widths.
+-/
+@[bv_normalize]
+def UnpackedFloat.proofRound {expWidth sigWidth : Nat}
+  {targetExponentWidth targetSignificandWidth : Nat}
+  (inUf : UnpackedFloat expWidth sigWidth)
+  (hTargetExponentWidth : targetExponentWidth ≤ expWidth)
+  (hSigWidth : targetSignificandWidth + 2 ≤ sigWidth)
+  (mode : RoundingMode) :
+  EUnpackedFloat (exponentWidth targetExponentWidth targetSignificandWidth) (targetSignificandWidth + 1) :=
+  -- round a normalized, normal float.
+  let exp : BitVec expWidth := inUf.ex
+
+  let targetMinNormalExp : BitVec expWidth :=
+    BitVec.ofInt expWidth (minNormalExp targetExponentWidth)
+
+  let hTargetMinNormalExp : targetMinNormalExp.toInt = minNormalExp targetExponentWidth := by
+    simp [targetMinNormalExp]
+    -- use 'fits' theorems from Fp/Theorems/Packing.
+    sorry
+  let earlyOverflow : Bool := exp.sgt (BitVec.ofInt expWidth (maxNormalExp targetExponentWidth))
+  let hEarlyOverflow : earlyOverflow =
+    decide (inUf.ex.toInt ≥ maxNormalExp targetExponentWidth) := sorry
+
+  -- early underflow:
+  let earlyUnderflow : Bool := exp.slt (BitVec.ofInt expWidth (minSubnormalExp targetExponentWidth targetSignificandWidth - 1))
+  let hEarlyUnderflow : earlyUnderflow =
+    decide (exp < minSubnormalExp targetExponentWidth targetSignificandWidth - 1) := sorry
+
+  -- force exponent to be at least min normal exponent.
+  let expGeMin :=
+    if exp.slt targetMinNormalExp then
+      targetMinNormalExp
+    else
+      exp
+  let hExpGeMin : expGeMin.toInt = max targetMinNormalExp.toInt exp.toInt := sorry
+
+  -- how much to shift 'sig' by.
+  let shiftAmtPositive := expGeMin - exp
+
+  let hShiftAmtPositive1 : shiftAmtPositive.toInt = expGeMin.toInt - exp.toInt := by sorry
+  let hShiftAmtPositive2 : shiftAmtPositive.toNat = expGeMin.toInt - exp.toInt := by sorry
+  -- have : shiftAmtPositive.toInt ≥ 0 := AxRoundNormal
+  -- have : shiftAmtPositive.toNat = shiftAmtPositive.toInt := AxRoundNormal
+  -- have : exp.toInt + shiftAmtPositive.toInt = expGeMin.toInt := AxRoundNormal
+
+  let sigWithHidden : BitVec sigWidth := inUf.sig
+
+  -- in inf precision, we want to take:
+  --                ↓ guard
+  --  1 . a b c d e f g h ... * 2^exp
+  --  ============↑ (6 bits of precision)
+  -- suppose we exceed by 3 bits, so shiftAmt = 3.
+
+  -- and convert to target precision:
+  --                  ↓ guard
+  --  0 . 0 0 0 1 a b c d e f g h * 2^exp + 2^shiftAmt | to make 'exp + shiftAmt >= minNormalExp'.
+  --  ==============↑ (6 bits of precision)
+  -- (sigWidth - 1) - (targetSignificandWidth - 1) -
+  -- let targetSigWithHidden : BitVec (targetSignificandWidth + 1) :=
+  --   sigWithHidden.extractMsb' 0 (targetSignificandWidth + 1)
+  -- to grab the bit *after* w bits, it's the bit x[w].
+  -- we want the bit *after* targetSignificandWidth + 1, i.e., bit at index targetSignificandWidth + 1.
+  let guardBitIndexFromLsb : BitVec sigWidth :=
+    BitVec.ofNat sigWidth ((sigWidth - 1) - (targetSignificandWidth + 1))
+  -- | See that when we call 'shiftAmtPositive.zeroExtend sigWidth', there is
+  -- a potential that shiftAmtPositive is wider than sigWidth.
+  -- However, when we compute early underflow,
+  let guardBitIndexFromLsbAdjusted : BitVec sigWidth :=
+    guardBitIndexFromLsb + shiftAmtPositive.zeroExtend sigWidth
+  -- TODO: figure out what to say about 'guardBitIndexFromLsb'?
+  let guardBitMask : BitVec sigWidth := BitVec.oneHotBV guardBitIndexFromLsbAdjusted
+  let guardBit : Bool := (sigWithHidden &&& guardBitMask) ≠ 0#sigWidth
+  -- TODO: guardBit ↔ ¬ isLower?
+  let stickyBitsMask : BitVec sigWidth := (BitVec.orderEncode guardBitIndexFromLsbAdjusted)
+  let stickyBits : BitVec sigWidth := (sigWithHidden &&& stickyBitsMask)
+  let stickyBit : Bool := stickyBits ≠ 0#sigWidth
+  -- TODO: guardbit => (stikyBit ↔ tieBreak)?
+  let sigwithHiddenCleared : BitVec sigWidth :=
+    sigWithHidden &&& (~~~(guardBitMask ||| stickyBitsMask))
+
+  let lsbMask : BitVec sigWidth :=
+     BitVec.oneHotBV (guardBitIndexFromLsbAdjusted + 1#sigWidth)
+
+  let isEven : Bool := sigWithHidden &&& lsbMask = 0#sigWidth
+  -- TODO: isEven ↔ isEven?
+  let shouldRoundUp := roundingDecision
+    (mode := mode)
+    (sign := inUf.sign)
+    (significandEven := isEven)
+    (guardBit := guardBit)
+    (stickyBit := stickyBit)
+    (_exact := false)
+  -- TODO: shouldRoundUp ↔ SMT-LIB shouldRoundUp?
+
+  let sigDidOverflow_RoundedTargetSigWithHidden : BitVec (sigWidth + 1) :=
+    if shouldRoundUp then
+      if sigwithHiddenCleared = 0#sigWidth && lsbMask = 0#sigWidth then
+        BitVec.oneHotBV (w := sigWidth + 1) (sigWidth)
+      else
+        sigwithHiddenCleared.zeroExtend (sigWidth + 1) + lsbMask.zeroExtend (sigWidth + 1)
+    else
+      sigwithHiddenCleared.zeroExtend (sigWidth + 1)
+
+  let sigDidOverflow : Bool :=
+    sigDidOverflow_RoundedTargetSigWithHidden.msb
+
+  let roundedTargetSigWithHidden : BitVec sigWidth :=
+    sigDidOverflow_RoundedTargetSigWithHidden.setWidth sigWidth
+
+
+  let roundedTargetSigWithHiddenOverflowAdjusted : BitVec sigWidth :=
+    if sigDidOverflow then
+      BitVec.leadingOne sigWidth
+    else
+      roundedTargetSigWithHidden
+  -- lower = upper + 1.
+  let roundedExpExtended : BitVec (expWidth + 1) :=
+    if sigDidOverflow then
+      exp.signExtend (expWidth + 1) + 1#(expWidth + 1)
+    else
+      exp.signExtend (expWidth + 1)
+
+  -- TODO: upper = lower + 1
+  -- I find this width stuff confusing, which width should we use?
+  -- have : expWidth ≥ exponentWidth targetExponentWidth targetSignificandWidth := by grind
+  let maxNormalExpBV : BitVec (expWidth + 1) :=
+    BitVec.ofInt (expWidth + 1) (maxNormalExp targetExponentWidth)
+  let lateOverflow : Bool :=
+    maxNormalExpBV.slt roundedExpExtended
+  -- let subnormalExpBV : BitVec (expWidth) := BitVec.ofInt (expWidth) (subnormalExp targetExponentWidth)
+  -- let minSubnormalExpMinusOneBV : BitVec (expWidth + 1) :=
+  --   BitVec.ofInt (expWidth + 1) (minSubnormalExp targetExponentWidth targetSignificandWidth - 1)
+  let minSubnormalExpBV : BitVec (expWidth + 1) :=
+    BitVec.ofInt (expWidth + 1) (minSubnormalExp targetExponentWidth targetSignificandWidth)
+  let lateUnderflow : Bool :=
+    roundedExpExtended.slt minSubnormalExpBV
+    -- (roundedExpExtended = minSubnormalExpMinusOneBV) && !shouldRoundUp
+  -- let out := out ++ s!"\nlateUnderflow: {lateUnderflow} = (roundedExpExtended({roundedExpExtended.toBitsStr}=int:{roundedExpExtended.toInt}) = minSubnormalExpMinusOneBV({minSubnormalExpMinusOneBV.toBitsStr}=int:{minSubnormalExpMinusOneBV.toInt}) - 1) && !shouldRoundUp({shouldRoundUp})"
+  -- let out := out ++ s!"\nlate underflow: {lateUnderflow} = roundedExp({roundedExp.toBitsStr}=int:{roundedExp.toInt}) < subnormalExpBV({subnormalExpBV.toBitsStr}=int:{subnormalExpBV.toInt})"
+  let underflow : Bool := lateUnderflow || earlyUnderflow
+  let overflow : Bool := lateOverflow || earlyOverflow
+
+  let roundedClampedExpExtended : BitVec (expWidth + 1) :=
+    if lateOverflow then
+      maxNormalExpBV
+    else if lateUnderflow then
+      minSubnormalExpBV
+    else
+      roundedExpExtended
+  let finalExp := roundedClampedExpExtended.truncate (exponentWidth targetExponentWidth targetSignificandWidth)
+  let finalSigTruncated := roundedTargetSigWithHiddenOverflowAdjusted.extractMsb' 0 (targetSignificandWidth + 1)
+  let finalNumber : UnpackedFloat (exponentWidth targetExponentWidth targetSignificandWidth) (targetSignificandWidth + 1) :=
+    { sign := inUf.sign,
+      ex := finalExp,
+      sig := finalSigTruncated
+    }
+  -- | TODO: I don't fully understand the special cases
+  let result := rounderSpecialCases
+    (roundingMode := mode)
+    (roundedResult := finalNumber)
+    (overflow := overflow)
+    (underflow := underflow)
+    (isZero := inUf.isZero)
+  result
+
+
 /-- Round an EUnpacked float, by ignoring NaN and infinity. -/
 def EUnpackedFloat.round {expWidth sigWidth : Nat} {targetExponentWidth targetSignificandWidth : Nat}
   (inEuf : EUnpackedFloat expWidth sigWidth)
diff --git a/Fp/Utils.lean b/Fp/Utils.lean
index 10b9727..56f877c 100644
--- a/Fp/Utils.lean
+++ b/Fp/Utils.lean
@@ -178,3 +178,52 @@ theorem Rat.two_pow_ne_zero (n : Int) : (2 : Rat) ^ n ≠ 0 := by
   apply Rat.ne_zero_of_zero_lt
   norm_cast
   grind
+
+theorem Rat.zpow_sub_eq_zpow_mul_zpow {b : Rat} (hb : b ≠ 0)
+    (x y: Int) : b ^ (x - y) = b ^ x * b ^ (-y) := by
+  rw [Int.sub_eq_add_neg]
+  rw [Rat.zpow_add hb]
+
+theorem Rat.mul_sub (b x y : Rat) : b * (x - y) = b * x - b * y := by
+  grind only
+
+@[simp, grind .]
+theorem Rat.one_le_two_pow_nat {n : Nat} : 1 ≤ (2 : Rat) ^ n := by
+  induction n with
+  | zero => grind
+  | succ n ih =>
+    rw [Rat.pow_succ]
+    grind
+
+theorem Rat.two_pow_le_two_pow_of_le {x y : Int} (h : x ≤ y) : (2 : Rat) ^ x ≤ (2 : Rat) ^ y := by
+  rw [Rat.le_iff_sub_nonneg]
+  rw [show (2 : Rat) ^ x = (2 : Rat) ^ x * 1 by grind only]
+  rw [show y = x + (y - x) by grind only]
+  rw [Rat.zpow_add (by grind only)]
+  rw [← Rat.mul_sub]
+  have : 1 ≤ (2 : Rat) ^ (y - x) := by
+    have : ∃ (k : Nat), y - x = k := by
+      exact Int.nonneg_def.mp h
+    obtain ⟨k, hk⟩ := this
+    rw [hk]
+    simp
+  grind only [Rat.mul_nonneg, Rat.le_of_lt, Fp.Rat.two_pow_pos]
+
+theorem Rat.le_mul_of_one_le_of_le  {x y y' : Rat} (hx1 : 1 ≤ x) (hy : 0 ≤ y) (hy' : y ≤ y')
+    : y ≤ x * y' := by
+  suffices 1 * y ≤ x * y' by grind only
+  apply Rat.mul_le_mul_of_le_of_le_of_nonneg_of_nonneg
+  · grind only
+  · grind only
+  · grind only [Rat.le_of_lt, Fp.Rat.two_pow_pos]
+  · grind only [Rat.le_of_lt, Fp.Rat.two_pow_pos]
+
+
+theorem Rat.le_mul_self_of_le_one_of_nonneg {y} {x : Rat} (hx0 : 0 ≤ x ∧ x ≤ 1) (hy : 0 ≤ y)
+    : x * y ≤ y := by
+  suffices x * y ≤ 1 * y by grind only
+  apply Rat.mul_le_mul_of_le_of_le_of_nonneg_of_nonneg
+  · grind only
+  · grind only
+  · grind only [Rat.le_of_lt, Fp.Rat.two_pow_pos]
+  · grind only [Rat.le_of_lt, Fp.Rat.two_pow_pos]
diff --git a/fp-real-theory/FpRealTheory/Smtlib.lean b/fp-real-theory/FpRealTheory/Smtlib.lean
index 647e90c..d6374db 100644
--- a/fp-real-theory/FpRealTheory/Smtlib.lean
+++ b/fp-real-theory/FpRealTheory/Smtlib.lean
@@ -149,7 +149,7 @@ noncomputable instance : ExtendedNumber ExtReal where
    isNaN r := r = .NaN
    smtLibEq r1 r2 := r1.eq r2
 
-instance : RoundableEmbed (PackedFloat e s) ExtReal where
+instance embedPackedFloatExtReal (e s : Nat) : RoundableEmbed (PackedFloat e s) ExtReal where
    embed := fun pf =>
       match pf.toExtRat with
       | .NaN => .NaN
@@ -159,7 +159,9 @@ instance : RoundableEmbed (PackedFloat e s) ExtReal where
 end ExtReal
 
 noncomputable def smtLibRealRounder : RoundMethod (PackedFloat e s) ExtReal :=
-   smtLibRoundMethod e s smtLibV smtLibV
+   smtLibRoundMethod e s
+      (smtLibV (ExtReal.embedPackedFloatExtReal e s))
+      (smtLibV (ExtReal.embedPackedFloatExtReal e (s + 1)))
 
 namespace RealSemantics
 open Classical