Theorem: s₃' (Fl.lean)

State before:
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
h : ulp n b ≤ 2 * a
⊢ b - trunc n (b - a) ≤ 2 * a
Tactic:
cases Nat.le_total a (ulp n b) with
| inl le_ulp => trans ulp n b
  . rewrite [tsub_le_iff_tsub_le]
    calc
      b - ulp n b
      _ = trunc n (b - ulp n b) := Eq.symm $ trunc_sub_ulp_eq_of_trunc_eq npos hfb
      _ ≤ trunc n (b - a)       := trunc_le_trunc npos $ tsub_le_tsub_left le_ulp _
  . exact h
| inr ulp_le => rewrite [Nat.two_mul, ← tsub_le_iff_right, tsub_right_comm, tsub_le_iff_left]
  calc
    b - a ≤ next n (trunc n (b - a))    := Nat.le_of_lt $ lt_next_trunc npos _
    _ = trunc n (b - a) + ulp n (b - a) := by unfold next ; rw [ulp_trunc npos _]
    _ ≤ trunc n (b - a) + ulp n b       := Nat.add_le_add_left (ulp_le_ulp n tsub_le_self) _
    _ ≤ trunc n (b - a) + a             := Nat.add_le_add_left ulp_le _
State after:
no goals

State before:
case inl
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
h : ulp n b ≤ 2 * a
le_ulp : a ≤ ulp n b
⊢ b - trunc n (b - a) ≤ 2 * a
Tactic:
trans ulp n b
State after:
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
h : ulp n b ≤ 2 * a
le_ulp : a ≤ ulp n b
⊢ b - trunc n (b - a) ≤ ulp n b

n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
h : ulp n b ≤ 2 * a
le_ulp : a ≤ ulp n b
⊢ ulp n b ≤ 2 * a

State before:
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
h : ulp n b ≤ 2 * a
le_ulp : a ≤ ulp n b
⊢ b - trunc n (b - a) ≤ ulp n b

n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
h : ulp n b ≤ 2 * a
le_ulp : a ≤ ulp n b
⊢ ulp n b ≤ 2 * a
Tactic:
. rewrite [tsub_le_iff_tsub_le]
  calc
    b - ulp n b
    _ = trunc n (b - ulp n b) := Eq.symm $ trunc_sub_ulp_eq_of_trunc_eq npos hfb
    _ ≤ trunc n (b - a)       := trunc_le_trunc npos $ tsub_le_tsub_left le_ulp _
State after:
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
h : ulp n b ≤ 2 * a
le_ulp : a ≤ ulp n b
⊢ ulp n b ≤ 2 * a

State before:
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
h : ulp n b ≤ 2 * a
le_ulp : a ≤ ulp n b
⊢ ulp n b ≤ 2 * a
Tactic:
. exact h
State after:
no goals

State before:
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
h : ulp n b ≤ 2 * a
le_ulp : a ≤ ulp n b
⊢ b - trunc n (b - a) ≤ ulp n b
Tactic:
rewrite [tsub_le_iff_tsub_le]
State after:
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
h : ulp n b ≤ 2 * a
le_ulp : a ≤ ulp n b
⊢ b - ulp n b ≤ trunc n (b - a)

State before:
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
h : ulp n b ≤ 2 * a
le_ulp : a ≤ ulp n b
⊢ b - ulp n b ≤ trunc n (b - a)
Tactic:
calc
  b - ulp n b
  _ = trunc n (b - ulp n b) := Eq.symm $ trunc_sub_ulp_eq_of_trunc_eq npos hfb
  _ ≤ trunc n (b - a)       := trunc_le_trunc npos $ tsub_le_tsub_left le_ulp _
State after:
no goals

State before:
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
h : ulp n b ≤ 2 * a
le_ulp : a ≤ ulp n b
⊢ ulp n b ≤ 2 * a
Tactic:
exact h
State after:
no goals

State before:
case inr
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
h : ulp n b ≤ 2 * a
ulp_le : ulp n b ≤ a
⊢ b - trunc n (b - a) ≤ 2 * a
Tactic:
rewrite [Nat.two_mul, ← tsub_le_iff_right, tsub_right_comm, tsub_le_iff_left]
State after:
case inr
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
h : ulp n b ≤ 2 * a
ulp_le : ulp n b ≤ a
⊢ b - a ≤ trunc n (b - a) + a

State before:
case inr
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
h : ulp n b ≤ 2 * a
ulp_le : ulp n b ≤ a
⊢ b - a ≤ trunc n (b - a) + a
Tactic:
calc
  b - a ≤ next n (trunc n (b - a))    := Nat.le_of_lt $ lt_next_trunc npos _
  _ = trunc n (b - a) + ulp n (b - a) := by unfold next ; rw [ulp_trunc npos _]
  _ ≤ trunc n (b - a) + ulp n b       := Nat.add_le_add_left (ulp_le_ulp n tsub_le_self) _
  _ ≤ trunc n (b - a) + a             := Nat.add_le_add_left ulp_le _
State after:
no goals

State before:
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
h : ulp n b ≤ 2 * a
ulp_le : ulp n b ≤ a
⊢ next n (trunc n (b - a)) = trunc n (b - a) + ulp n (b - a)
Tactic:
unfold next
State after:
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
h : ulp n b ≤ 2 * a
ulp_le : ulp n b ≤ a
⊢ trunc n (b - a) + ulp n (trunc n (b - a)) = trunc n (b - a) + ulp n (b - a)

State before:
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
h : ulp n b ≤ 2 * a
ulp_le : ulp n b ≤ a
⊢ trunc n (b - a) + ulp n (trunc n (b - a)) = trunc n (b - a) + ulp n (b - a)
Tactic:
rw [ulp_trunc npos _]
State after:
no goals