Theorem: ulp_next_of_no_carry (Fl/Trunc.lean)

State before:
n x : ℕ
no_carry : next n x < 2 ^ Nat.size x
⊢ ulp n (next n x) = ulp n x
Tactic:
unfold ulp expt
State after:
n x : ℕ
no_carry : next n x < 2 ^ Nat.size x
⊢ 2 ^ (Nat.size (next n x) - n) = 2 ^ (Nat.size x - n)

State before:
n x : ℕ
no_carry : next n x < 2 ^ Nat.size x
⊢ 2 ^ (Nat.size (next n x) - n) = 2 ^ (Nat.size x - n)
Tactic:
rw [size_next_eq_size_of_no_carry no_carry]
State after:
no goals