Theorem: b₁_lo_of_of_round_le_of_no_uflow_of_of_ulp_le (Fl.lean)

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
⊢ trunc n (a - b - round (a - b)) = a - b - round (a - b)
Tactic:
have hca : round (a - b) ≤ a := round_sub_le npos hfaithful₀ hfaithful₁ b hfa
State after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
⊢ trunc n (a - b - round (a - b)) = a - b - round (a - b)

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
⊢ trunc n (a - b - round (a - b)) = a - b - round (a - b)
Tactic:
have ulp_even : 2 ∣ ulp n (a - b) := two_dvd_ulp_of_no_uflow no_uflow
State after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ trunc n (a - b - round (a - b)) = a - b - round (a - b)

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ trunc n (a - b - round (a - b)) = a - b - round (a - b)
Tactic:
have hfd : trunc n (a - round (a - b) - b) = a - round (a - b) - b := by
  apply sterbenz
  . exact s₂ npos hfaithful₀ hfaithful₁ hfa hfb hba
  . exact hfb
  . rewrite [le_tsub_iff_left hca, ← le_tsub_iff_right hba]
    exact round_le
  . rewrite [round_eq_trunc_of_le npos hfaithful₁ round_le]
    rewrite [Nat.two_mul]
    rewrite [← tsub_le_iff_left]
    rewrite [tsub_right_comm]
    trans ulp n (a - b) / 2
    . rewrite [tsub_le_iff_left]
      apply le_midpoint_of_round_eq_trunc npos hcorrect₀
      exact round_eq_trunc_of_le npos hfaithful₁ round_le
    . refine Nat.le_of_mul_le_mul_left ?_ two_pos
      rewrite [Nat.mul_comm, Nat.div_mul_cancel ulp_even]
      exact ulp_le'
State after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
hfd : trunc n (a - round (a - b) - b) = a - round (a - b) - b
⊢ trunc n (a - b - round (a - b)) = a - b - round (a - b)

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
hfd : trunc n (a - round (a - b) - b) = a - round (a - b) - b
⊢ trunc n (a - b - round (a - b)) = a - b - round (a - b)
Tactic:
rewrite [eq_tsub_iff_add_eq_of_le round_le]
State after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
hfd : trunc n (a - round (a - b) - b) = a - round (a - b) - b
⊢ trunc n (a - b - round (a - b)) + round (a - b) = a - b

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
hfd : trunc n (a - round (a - b) - b) = a - round (a - b) - b
⊢ trunc n (a - b - round (a - b)) + round (a - b) = a - b
Tactic:
rewrite [add_comm]
State after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
hfd : trunc n (a - round (a - b) - b) = a - round (a - b) - b
⊢ round (a - b) + trunc n (a - b - round (a - b)) = a - b

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
hfd : trunc n (a - round (a - b) - b) = a - round (a - b) - b
⊢ round (a - b) + trunc n (a - b - round (a - b)) = a - b
Tactic:
rewrite [tsub_right_comm]
State after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
hfd : trunc n (a - round (a - b) - b) = a - round (a - b) - b
⊢ round (a - b) + trunc n (a - round (a - b) - b) = a - b

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
hfd : trunc n (a - round (a - b) - b) = a - round (a - b) - b
⊢ round (a - b) + trunc n (a - round (a - b) - b) = a - b
Tactic:
rewrite [hfd]
State after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
hfd : trunc n (a - round (a - b) - b) = a - round (a - b) - b
⊢ round (a - b) + (a - round (a - b) - b) = a - b

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
hfd : trunc n (a - round (a - b) - b) = a - round (a - b) - b
⊢ round (a - b) + (a - round (a - b) - b) = a - b
Tactic:
rewrite [tsub_right_comm]
State after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
hfd : trunc n (a - round (a - b) - b) = a - round (a - b) - b
⊢ round (a - b) + (a - b - round (a - b)) = a - b

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
hfd : trunc n (a - round (a - b) - b) = a - round (a - b) - b
⊢ round (a - b) + (a - b - round (a - b)) = a - b
Tactic:
exact add_tsub_cancel_of_le round_le
State after:
no goals

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ trunc n (a - round (a - b) - b) = a - round (a - b) - b
Tactic:
apply sterbenz
State after:
case hfa
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ trunc n (a - round (a - b)) = a - round (a - b)

case hfb
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ trunc n b = b

case hba
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ b ≤ a - round (a - b)

case hab
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ a - round (a - b) ≤ 2 * b

State before:
case hfa
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ trunc n (a - round (a - b)) = a - round (a - b)

case hfb
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ trunc n b = b

case hba
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ b ≤ a - round (a - b)

case hab
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ a - round (a - b) ≤ 2 * b
Tactic:
. exact s₂ npos hfaithful₀ hfaithful₁ hfa hfb hba
State after:
case hfb
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ trunc n b = b

case hba
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ b ≤ a - round (a - b)

case hab
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ a - round (a - b) ≤ 2 * b

State before:
case hfb
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ trunc n b = b

case hba
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ b ≤ a - round (a - b)

case hab
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ a - round (a - b) ≤ 2 * b
Tactic:
. exact hfb
State after:
case hba
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ b ≤ a - round (a - b)

case hab
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ a - round (a - b) ≤ 2 * b

State before:
case hba
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ b ≤ a - round (a - b)

case hab
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ a - round (a - b) ≤ 2 * b
Tactic:
. rewrite [le_tsub_iff_left hca, ← le_tsub_iff_right hba]
  exact round_le
State after:
case hab
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ a - round (a - b) ≤ 2 * b

State before:
case hab
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ a - round (a - b) ≤ 2 * b
Tactic:
. rewrite [round_eq_trunc_of_le npos hfaithful₁ round_le]
  rewrite [Nat.two_mul]
  rewrite [← tsub_le_iff_left]
  rewrite [tsub_right_comm]
  trans ulp n (a - b) / 2
  . rewrite [tsub_le_iff_left]
    apply le_midpoint_of_round_eq_trunc npos hcorrect₀
    exact round_eq_trunc_of_le npos hfaithful₁ round_le
  . refine Nat.le_of_mul_le_mul_left ?_ two_pos
    rewrite [Nat.mul_comm, Nat.div_mul_cancel ulp_even]
    exact ulp_le'
State after:
no goals

State before:
case hfa
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ trunc n (a - round (a - b)) = a - round (a - b)
Tactic:
exact s₂ npos hfaithful₀ hfaithful₁ hfa hfb hba
State after:
no goals

State before:
case hfb
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ trunc n b = b
Tactic:
exact hfb
State after:
no goals

State before:
case hba
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ b ≤ a - round (a - b)
Tactic:
rewrite [le_tsub_iff_left hca, ← le_tsub_iff_right hba]
State after:
case hba
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ round (a - b) ≤ a - b

State before:
case hba
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ round (a - b) ≤ a - b
Tactic:
exact round_le
State after:
no goals

State before:
case hab
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ a - round (a - b) ≤ 2 * b
Tactic:
rewrite [round_eq_trunc_of_le npos hfaithful₁ round_le]
State after:
case hab
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ a - trunc n (a - b) ≤ 2 * b

State before:
case hab
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ a - trunc n (a - b) ≤ 2 * b
Tactic:
rewrite [Nat.two_mul]
State after:
case hab
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ a - trunc n (a - b) ≤ b + b

State before:
case hab
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ a - trunc n (a - b) ≤ b + b
Tactic:
rewrite [← tsub_le_iff_left]
State after:
case hab
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ a - trunc n (a - b) - b ≤ b

State before:
case hab
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ a - trunc n (a - b) - b ≤ b
Tactic:
rewrite [tsub_right_comm]
State after:
case hab
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ a - b - trunc n (a - b) ≤ b

State before:
case hab
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ a - b - trunc n (a - b) ≤ b
Tactic:
trans ulp n (a - b) / 2
State after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ a - b - trunc n (a - b) ≤ ulp n (a - b) / 2

round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ ulp n (a - b) / 2 ≤ b

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ a - b - trunc n (a - b) ≤ ulp n (a - b) / 2

round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ ulp n (a - b) / 2 ≤ b
Tactic:
. rewrite [tsub_le_iff_left]
  apply le_midpoint_of_round_eq_trunc npos hcorrect₀
  exact round_eq_trunc_of_le npos hfaithful₁ round_le
State after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ ulp n (a - b) / 2 ≤ b

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ ulp n (a - b) / 2 ≤ b
Tactic:
. refine Nat.le_of_mul_le_mul_left ?_ two_pos
  rewrite [Nat.mul_comm, Nat.div_mul_cancel ulp_even]
  exact ulp_le'
State after:
no goals

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ a - b - trunc n (a - b) ≤ ulp n (a - b) / 2
Tactic:
rewrite [tsub_le_iff_left]
State after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ a - b ≤ trunc n (a - b) + ulp n (a - b) / 2

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ a - b ≤ trunc n (a - b) + ulp n (a - b) / 2
Tactic:
apply le_midpoint_of_round_eq_trunc npos hcorrect₀
State after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ round (a - b) = trunc n (a - b)

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ round (a - b) = trunc n (a - b)
Tactic:
exact round_eq_trunc_of_le npos hfaithful₁ round_le
State after:
no goals

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ ulp n (a - b) / 2 ≤ b
Tactic:
refine Nat.le_of_mul_le_mul_left ?_ two_pos
State after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ 2 * (ulp n (a - b) / 2) ≤ 2 * b

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ 2 * (ulp n (a - b) / 2) ≤ 2 * b
Tactic:
rewrite [Nat.mul_comm, Nat.div_mul_cancel ulp_even]
State after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ ulp n (a - b) ≤ 2 * b

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
no_uflow : a - b ≥ 2 ^ n
ulp_le' : ulp n (a - b) ≤ 2 * b
hca : round (a - b) ≤ a
ulp_even : 2 ∣ ulp n (a - b)
⊢ ulp n (a - b) ≤ 2 * b
Tactic:
exact ulp_le'
State after:
no goals