Theorem: ulp_sub_le_of_two_mul_le_of_lt_round (Fl.lean)

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
⊢ ulp n (a - b) - (a - b) % ulp n (a - b) ≤ b
Tactic:
have hba' : b ≤ a := Nat.le_trans (Nat.le_mul_of_pos_left two_pos) hba
State after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
⊢ ulp n (a - b) - (a - b) % ulp n (a - b) ≤ b

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
⊢ ulp n (a - b) - (a - b) % ulp n (a - b) ≤ b
Tactic:
have h₁ : a ≤ b + round (a - b) := by
  trans b + (a - b)
  . rewrite [← add_tsub_assoc_of_le hba']
    exact Nat.le_of_eq $ Eq.symm $ add_tsub_cancel_left _ _
  . apply Nat.add_le_add_left
    exact lt_round.le
State after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
h₁ : a ≤ b + round (a - b)
⊢ ulp n (a - b) - (a - b) % ulp n (a - b) ≤ b

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
h₁ : a ≤ b + round (a - b)
⊢ ulp n (a - b) - (a - b) % ulp n (a - b) ≤ b
Tactic:
have h₂ : a ≤ round (a - b) + b := by rwa [Nat.add_comm]
State after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
h₁ : a ≤ b + round (a - b)
h₂ : a ≤ round (a - b) + b
⊢ ulp n (a - b) - (a - b) % ulp n (a - b) ≤ b

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
h₁ : a ≤ b + round (a - b)
h₂ : a ≤ round (a - b) + b
⊢ ulp n (a - b) - (a - b) % ulp n (a - b) ≤ b
Tactic:
have h₃ : 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
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
h₁ : a ≤ b + round (a - b)
h₂ : a ≤ round (a - b) + b
h₃ : round (a - b) ≤ a
⊢ ulp n (a - b) - (a - b) % ulp n (a - b) ≤ b

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
h₁ : a ≤ b + round (a - b)
h₂ : a ≤ round (a - b) + b
h₃ : round (a - b) ≤ a
⊢ ulp n (a - b) - (a - b) % ulp n (a - b) ≤ b
Tactic:
rewrite [← next_trunc_sub_eq_ulp_sub_mod npos]
State after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
h₁ : a ≤ b + round (a - b)
h₂ : a ≤ round (a - b) + b
h₃ : round (a - b) ≤ a
⊢ next n (trunc n (a - b)) - (a - b) ≤ b

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
h₁ : a ≤ b + round (a - b)
h₂ : a ≤ round (a - b) + b
h₃ : round (a - b) ≤ a
⊢ next n (trunc n (a - b)) - (a - b) ≤ b
Tactic:
rewrite [← round_eq_next_trunc_of_gt hfaithful₁ lt_round]
State after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
h₁ : a ≤ b + round (a - b)
h₂ : a ≤ round (a - b) + b
h₃ : round (a - b) ≤ a
⊢ round (a - b) - (a - b) ≤ b

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
h₁ : a ≤ b + round (a - b)
h₂ : a ≤ round (a - b) + b
h₃ : round (a - b) ≤ a
⊢ round (a - b) - (a - b) ≤ b
Tactic:
rewrite [← add_tsub_assoc' h₁ hba']
State after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
h₁ : a ≤ b + round (a - b)
h₂ : a ≤ round (a - b) + b
h₃ : 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
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
h₁ : a ≤ b + round (a - b)
h₂ : a ≤ round (a - b) + b
h₃ : round (a - b) ≤ a
⊢ round (a - b) + b - a ≤ b
Tactic:
rewrite [Nat.add_comm]
State after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
h₁ : a ≤ b + round (a - b)
h₂ : a ≤ round (a - b) + b
h₃ : 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
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
h₁ : a ≤ b + round (a - b)
h₂ : a ≤ round (a - b) + b
h₃ : round (a - b) ≤ a
⊢ b + round (a - b) - a ≤ b
Tactic:
rewrite [add_tsub_assoc' h₂ h₃]
State after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
h₁ : a ≤ b + round (a - b)
h₂ : a ≤ round (a - b) + b
h₃ : round (a - b) ≤ a
⊢ b - (a - round (a - b)) ≤ b

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
h₁ : a ≤ b + round (a - b)
h₂ : a ≤ round (a - b) + b
h₃ : round (a - b) ≤ a
⊢ b - (a - round (a - b)) ≤ b
Tactic:
exact tsub_le_self
State after:
no goals

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
⊢ a ≤ b + round (a - b)
Tactic:
trans b + (a - b)
State after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
⊢ a ≤ b + (a - b)

round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
⊢ b + (a - b) ≤ b + round (a - b)

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
⊢ a ≤ b + (a - b)

round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
⊢ b + (a - b) ≤ b + round (a - b)
Tactic:
. rewrite [← add_tsub_assoc_of_le hba']
  exact Nat.le_of_eq $ Eq.symm $ add_tsub_cancel_left _ _
State after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
⊢ b + (a - b) ≤ b + round (a - b)

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
⊢ b + (a - b) ≤ b + round (a - b)
Tactic:
. apply Nat.add_le_add_left
  exact lt_round.le
State after:
no goals

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
⊢ a ≤ b + (a - b)
Tactic:
rewrite [← add_tsub_assoc_of_le hba']
State after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
⊢ a ≤ b + a - b

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
⊢ a ≤ b + a - b
Tactic:
exact Nat.le_of_eq $ Eq.symm $ add_tsub_cancel_left _ _
State after:
no goals

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
⊢ b + (a - b) ≤ b + round (a - b)
Tactic:
apply Nat.add_le_add_left
State after:
case h
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
⊢ a - b ≤ round (a - b)

State before:
case h
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
⊢ a - b ≤ round (a - b)
Tactic:
exact lt_round.le
State after:
no goals

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : 2 * b ≤ a
lt_round : a - b < round (a - b)
hba' : b ≤ a
h₁ : a ≤ b + round (a - b)
⊢ a ≤ round (a - b) + b
Tactic:
rwa [Nat.add_comm]
State after:
no goals