Theorem: b₁_lo_of_round_lt_of_no_uflow_of_ulp_eq_ulp_of_two_mul_lt_of_pos_of_le_ulp (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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
⊢ trunc n (a - b - round (a - b)) = a - b - round (a - b)
Tactic:
apply b₁_lo_of_round_lt_of_ulp_le npos hfaithful₀ hfaithful₁ hfa hfb hba round_lt
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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
⊢ ulp n a ≤ 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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
⊢ ulp n a ≤ 2 * b
Tactic:
have apos : 0 < a := Nat.lt_of_lt_of_le two_pow_pos $ Nat.le_trans no_uflow tsub_le_self
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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
⊢ ulp n a ≤ 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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
⊢ ulp n a ≤ 2 * b
Tactic:
have ulp_even : 2 ∣ ulp n a :=
  two_dvd_ulp_of_no_uflow $ Nat.le_trans no_uflow tsub_le_self
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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
⊢ ulp n a ≤ 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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
⊢ ulp n a ≤ 2 * b
Tactic:
have h₁ : round (a - b) = trunc n (a - b) := round_eq_trunc_of_le npos hfaithful₁ round_lt.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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
⊢ ulp n a ≤ 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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
⊢ ulp n a ≤ 2 * b
Tactic:
have h₂ : (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 2 := by
  rewrite [← tsub_le_tsub_iff_left (Nat.mod_le _ _)]
  rewrite [← trunc_eq_sub_mod]
  rewrite [tsub_le_iff_right]
  exact le_midpoint_of_round_eq_trunc npos hcorrect₀ h₁
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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
h₂ : (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 2
⊢ ulp n a ≤ 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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
h₂ : (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 2
⊢ ulp n a ≤ 2 * b
Tactic:
have h₃ : a - b = a - ulp n a + (ulp n a - b) := by
   rewrite [← add_tsub_assoc_of_le le_ulp]
   rw [tsub_add_cancel_of_le $ ulp_le_self npos apos]
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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
h₂ : (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 2
h₃ : a - b = a - ulp n a + (ulp n a - b)
⊢ ulp n a ≤ 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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
h₂ : (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 2
h₃ : a - b = a - ulp n a + (ulp n a - b)
⊢ ulp n a ≤ 2 * b
Tactic:
have h₄ : (a - b) % ulp n (a - b) = ulp n a - b := by
  rewrite [ulp_eq_ulp]
  rewrite [h₃]
  rewrite [← Nat.mod_add_mod]
  rewrite [mod_sub_mod _ _ _ (ulp_le_self npos apos)]
  rewrite [Nat.mod_self, tsub_zero]
  rewrite [Nat.mod_eq_zero_of_dvd (ulp_dvd_of_trunc_eq hfa), Nat.zero_add]
  exact Nat.mod_eq_of_lt (tsub_lt_self (ulp_pos _ _) bpos)
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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
h₂ : (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 2
h₃ : a - b = a - ulp n a + (ulp n a - b)
h₄ : (a - b) % ulp n (a - b) = ulp n a - b
⊢ ulp n a ≤ 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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
h₂ : (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 2
h₃ : a - b = a - ulp n a + (ulp n a - b)
h₄ : (a - b) % ulp n (a - b) = ulp n a - b
⊢ ulp n a ≤ 2 * b
Tactic:
have h₅ : ulp n a - b ≤ ulp n a / 2 := by
  rewrite [← h₄]
  rewrite [← ulp_eq_ulp]
  exact h₂
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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
h₂ : (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 2
h₃ : a - b = a - ulp n a + (ulp n a - b)
h₄ : (a - b) % ulp n (a - b) = ulp n a - b
h₅ : ulp n a - b ≤ ulp n a / 2
⊢ ulp n a ≤ 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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
h₂ : (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 2
h₃ : a - b = a - ulp n a + (ulp n a - b)
h₄ : (a - b) % ulp n (a - b) = ulp n a - b
h₅ : ulp n a - b ≤ ulp n a / 2
⊢ ulp n a ≤ 2 * b
Tactic:
have h₆ : ulp n a / 2 ≤ b := by
  rewrite [← tsub_tsub_cancel_of_le le_ulp]
  rewrite [← sub_half_of_even ulp_even]
  apply tsub_le_tsub_left
  exact h₅
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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
h₂ : (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 2
h₃ : a - b = a - ulp n a + (ulp n a - b)
h₄ : (a - b) % ulp n (a - b) = ulp n a - b
h₅ : ulp n a - b ≤ ulp n a / 2
h₆ : ulp n a / 2 ≤ b
⊢ ulp n a ≤ 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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
h₂ : (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 2
h₃ : a - b = a - ulp n a + (ulp n a - b)
h₄ : (a - b) % ulp n (a - b) = ulp n a - b
h₅ : ulp n a - b ≤ ulp n a / 2
h₆ : ulp n a / 2 ≤ b
⊢ ulp n a ≤ 2 * b
Tactic:
rewrite [Nat.two_mul]
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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
h₂ : (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 2
h₃ : a - b = a - ulp n a + (ulp n a - b)
h₄ : (a - b) % ulp n (a - b) = ulp n a - b
h₅ : ulp n a - b ≤ ulp n a / 2
h₆ : ulp n a / 2 ≤ b
⊢ ulp n a ≤ b + 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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
h₂ : (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 2
h₃ : a - b = a - ulp n a + (ulp n a - b)
h₄ : (a - b) % ulp n (a - b) = ulp n a - b
h₅ : ulp n a - b ≤ ulp n a / 2
h₆ : ulp n a / 2 ≤ b
⊢ ulp n a ≤ b + b
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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
h₂ : (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 2
h₃ : a - b = a - ulp n a + (ulp n a - b)
h₄ : (a - b) % ulp n (a - b) = ulp n a - b
h₅ : ulp n a - b ≤ ulp n a / 2
h₆ : ulp n a / 2 ≤ b
⊢ ulp n a - b ≤ 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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
h₂ : (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 2
h₃ : a - b = a - ulp n a + (ulp n a - b)
h₄ : (a - b) % ulp n (a - b) = ulp n a - b
h₅ : ulp n a - b ≤ ulp n a / 2
h₆ : ulp n a / 2 ≤ b
⊢ ulp n a - b ≤ b
Tactic:
trans ulp n a / 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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
h₂ : (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 2
h₃ : a - b = a - ulp n a + (ulp n a - b)
h₄ : (a - b) % ulp n (a - b) = ulp n a - b
h₅ : ulp n a - b ≤ ulp n a / 2
h₆ : ulp n a / 2 ≤ b
⊢ ulp n a - b ≤ ulp n a / 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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
h₂ : (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 2
h₃ : a - b = a - ulp n a + (ulp n a - b)
h₄ : (a - b) % ulp n (a - b) = ulp n a - b
h₅ : ulp n a - b ≤ ulp n a / 2
h₆ : ulp n a / 2 ≤ b
⊢ ulp n a / 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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
h₂ : (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 2
h₃ : a - b = a - ulp n a + (ulp n a - b)
h₄ : (a - b) % ulp n (a - b) = ulp n a - b
h₅ : ulp n a - b ≤ ulp n a / 2
h₆ : ulp n a / 2 ≤ b
⊢ ulp n a - b ≤ ulp n a / 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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
h₂ : (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 2
h₃ : a - b = a - ulp n a + (ulp n a - b)
h₄ : (a - b) % ulp n (a - b) = ulp n a - b
h₅ : ulp n a - b ≤ ulp n a / 2
h₆ : ulp n a / 2 ≤ b
⊢ ulp n a / 2 ≤ b
Tactic:
. exact h₅
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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
h₂ : (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 2
h₃ : a - b = a - ulp n a + (ulp n a - b)
h₄ : (a - b) % ulp n (a - b) = ulp n a - b
h₅ : ulp n a - b ≤ ulp n a / 2
h₆ : ulp n a / 2 ≤ b
⊢ ulp n a / 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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
h₂ : (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 2
h₃ : a - b = a - ulp n a + (ulp n a - b)
h₄ : (a - b) % ulp n (a - b) = ulp n a - b
h₅ : ulp n a - b ≤ ulp n a / 2
h₆ : ulp n a / 2 ≤ b
⊢ ulp n a / 2 ≤ b
Tactic:
. exact h₆
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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
⊢ (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 2
Tactic:
rewrite [← tsub_le_tsub_iff_left (Nat.mod_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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
⊢ a - b - ulp n (a - b) / 2 ≤ a - b - (a - b) % ulp 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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
⊢ a - b - ulp n (a - b) / 2 ≤ a - b - (a - b) % ulp n (a - b)
Tactic:
rewrite [← trunc_eq_sub_mod]
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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
⊢ a - b - ulp n (a - b) / 2 ≤ 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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
⊢ a - b - ulp n (a - b) / 2 ≤ trunc n (a - b)
Tactic:
rewrite [tsub_le_iff_right]
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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc 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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
⊢ a - b ≤ trunc n (a - b) + ulp n (a - b) / 2
Tactic:
exact le_midpoint_of_round_eq_trunc npos hcorrect₀ h₁
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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
h₂ : (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 2
⊢ a - b = a - ulp n a + (ulp n a - b)
Tactic:
rewrite [← add_tsub_assoc_of_le le_ulp]
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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
h₂ : (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 2
⊢ a - b = a - ulp n a + ulp 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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
h₂ : (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 2
⊢ a - b = a - ulp n a + ulp n a - b
Tactic:
rw [tsub_add_cancel_of_le $ ulp_le_self npos apos]
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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
h₂ : (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 2
h₃ : a - b = a - ulp n a + (ulp n a - b)
⊢ (a - b) % ulp n (a - b) = ulp n a - b
Tactic:
rewrite [ulp_eq_ulp]
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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
h₂ : (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 2
h₃ : a - b = a - ulp n a + (ulp n a - b)
⊢ (a - b) % ulp n a = ulp 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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
h₂ : (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 2
h₃ : a - b = a - ulp n a + (ulp n a - b)
⊢ (a - b) % ulp n a = ulp n a - b
Tactic:
rewrite [h₃]
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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
h₂ : (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 2
h₃ : a - b = a - ulp n a + (ulp n a - b)
⊢ (a - ulp n a + (ulp n a - b)) % ulp n a = ulp 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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
h₂ : (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 2
h₃ : a - b = a - ulp n a + (ulp n a - b)
⊢ (a - ulp n a + (ulp n a - b)) % ulp n a = ulp n a - b
Tactic:
rewrite [← Nat.mod_add_mod]
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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
h₂ : (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 2
h₃ : a - b = a - ulp n a + (ulp n a - b)
⊢ ((a - ulp n a) % ulp n a + (ulp n a - b)) % ulp n a = ulp 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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
h₂ : (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 2
h₃ : a - b = a - ulp n a + (ulp n a - b)
⊢ ((a - ulp n a) % ulp n a + (ulp n a - b)) % ulp n a = ulp n a - b
Tactic:
rewrite [mod_sub_mod _ _ _ (ulp_le_self npos apos)]
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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
h₂ : (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 2
h₃ : a - b = a - ulp n a + (ulp n a - b)
⊢ ((a - ulp n a % ulp n a) % ulp n a + (ulp n a - b)) % ulp n a = ulp 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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
h₂ : (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 2
h₃ : a - b = a - ulp n a + (ulp n a - b)
⊢ ((a - ulp n a % ulp n a) % ulp n a + (ulp n a - b)) % ulp n a = ulp n a - b
Tactic:
rewrite [Nat.mod_self, tsub_zero]
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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
h₂ : (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 2
h₃ : a - b = a - ulp n a + (ulp n a - b)
⊢ (a % ulp n a + (ulp n a - b)) % ulp n a = ulp 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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
h₂ : (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 2
h₃ : a - b = a - ulp n a + (ulp n a - b)
⊢ (a % ulp n a + (ulp n a - b)) % ulp n a = ulp n a - b
Tactic:
rewrite [Nat.mod_eq_zero_of_dvd (ulp_dvd_of_trunc_eq hfa), Nat.zero_add]
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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
h₂ : (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 2
h₃ : a - b = a - ulp n a + (ulp n a - b)
⊢ (ulp n a - b) % ulp n a = ulp 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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
h₂ : (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 2
h₃ : a - b = a - ulp n a + (ulp n a - b)
⊢ (ulp n a - b) % ulp n a = ulp n a - b
Tactic:
exact Nat.mod_eq_of_lt (tsub_lt_self (ulp_pos _ _) bpos)
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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
h₂ : (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 2
h₃ : a - b = a - ulp n a + (ulp n a - b)
h₄ : (a - b) % ulp n (a - b) = ulp n a - b
⊢ ulp n a - b ≤ ulp n a / 2
Tactic:
rewrite [← h₄]
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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
h₂ : (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 2
h₃ : a - b = a - ulp n a + (ulp n a - b)
h₄ : (a - b) % ulp n (a - b) = ulp n a - b
⊢ (a - b) % ulp n (a - b) ≤ ulp n a / 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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
h₂ : (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 2
h₃ : a - b = a - ulp n a + (ulp n a - b)
h₄ : (a - b) % ulp n (a - b) = ulp n a - b
⊢ (a - b) % ulp n (a - b) ≤ ulp n a / 2
Tactic:
rewrite [← ulp_eq_ulp]
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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
h₂ : (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 2
h₃ : a - b = a - ulp n a + (ulp n a - b)
h₄ : (a - b) % ulp n (a - b) = ulp n a - b
⊢ (a - b) % ulp 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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
h₂ : (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 2
h₃ : a - b = a - ulp n a + (ulp n a - b)
h₄ : (a - b) % ulp n (a - b) = ulp n a - b
⊢ (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 2
Tactic:
exact h₂
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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
h₂ : (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 2
h₃ : a - b = a - ulp n a + (ulp n a - b)
h₄ : (a - b) % ulp n (a - b) = ulp n a - b
h₅ : ulp n a - b ≤ ulp n a / 2
⊢ ulp n a / 2 ≤ b
Tactic:
rewrite [← tsub_tsub_cancel_of_le le_ulp]
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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
h₂ : (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 2
h₃ : a - b = a - ulp n a + (ulp n a - b)
h₄ : (a - b) % ulp n (a - b) = ulp n a - b
h₅ : ulp n a - b ≤ ulp n a / 2
⊢ ulp n a / 2 ≤ ulp n a - (ulp 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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
h₂ : (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 2
h₃ : a - b = a - ulp n a + (ulp n a - b)
h₄ : (a - b) % ulp n (a - b) = ulp n a - b
h₅ : ulp n a - b ≤ ulp n a / 2
⊢ ulp n a / 2 ≤ ulp n a - (ulp n a - b)
Tactic:
rewrite [← sub_half_of_even 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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
h₂ : (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 2
h₃ : a - b = a - ulp n a + (ulp n a - b)
h₄ : (a - b) % ulp n (a - b) = ulp n a - b
h₅ : ulp n a - b ≤ ulp n a / 2
⊢ ulp n a - ulp n a / 2 ≤ ulp n a - (ulp 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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
h₂ : (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 2
h₃ : a - b = a - ulp n a + (ulp n a - b)
h₄ : (a - b) % ulp n (a - b) = ulp n a - b
h₅ : ulp n a - b ≤ ulp n a / 2
⊢ ulp n a - ulp n a / 2 ≤ ulp n a - (ulp n a - b)
Tactic:
apply tsub_le_tsub_left
State after:
case h
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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
h₂ : (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 2
h₃ : a - b = a - ulp n a + (ulp n a - b)
h₄ : (a - b) % ulp n (a - b) = ulp n a - b
h₅ : ulp n a - b ≤ ulp n a / 2
⊢ ulp n a - b ≤ ulp n a / 2

State before:
case h
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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
h₂ : (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 2
h₃ : a - b = a - ulp n a + (ulp n a - b)
h₄ : (a - b) % ulp n (a - b) = ulp n a - b
h₅ : ulp n a - b ≤ ulp n a / 2
⊢ ulp n a - b ≤ ulp n a / 2
Tactic:
exact h₅
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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
h₂ : (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 2
h₃ : a - b = a - ulp n a + (ulp n a - b)
h₄ : (a - b) % ulp n (a - b) = ulp n a - b
h₅ : ulp n a - b ≤ ulp n a / 2
h₆ : ulp n a / 2 ≤ b
⊢ ulp n a - b ≤ ulp n a / 2
Tactic:
exact h₅
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_lt : round (a - b) < a - b
no_uflow : 2 ^ n ≤ a - b
ulp_eq_ulp : ulp n (a - b) = ulp n a
bpos : b > 0
le_ulp : b ≤ ulp n a
apos : 0 < a
ulp_even : 2 ∣ ulp n a
h₁ : round (a - b) = trunc n (a - b)
h₂ : (a - b) % ulp n (a - b) ≤ ulp n (a - b) / 2
h₃ : a - b = a - ulp n a + (ulp n a - b)
h₄ : (a - b) % ulp n (a - b) = ulp n a - b
h₅ : ulp n a - b ≤ ulp n a / 2
h₆ : ulp n a / 2 ≤ b
⊢ ulp n a / 2 ≤ b
Tactic:
exact h₆
State after:
no goals