Theorem: b₁_lo_of_round_lt_of_ulp_le (Fl.lean)

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
ulp_le : ulp n a ≤ 2 * b
⊢ trunc n (a - b - round (a - b)) = a - b - round (a - b)
Tactic:
have hfe : round (a - round (a - b)) = a - round (a - b) := by
  apply round_eq_of_trunc_eq npos hfaithful₀
  apply s₂ npos hfaithful₀ hfaithful₁ hfa hfb hba
State after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
ulp_le : ulp n a ≤ 2 * b
hfe : round (a - round (a - b)) = a - round (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
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
ulp_le : ulp n a ≤ 2 * b
hfe : round (a - round (a - b)) = a - round (a - b)
⊢ trunc n (a - b - round (a - b)) = a - b - round (a - b)
Tactic:
have h₀ : b < round (a - round (a - b)) := by
  rewrite [hfe]
  rewrite [lt_tsub_comm]
  exact round_lt
State after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
ulp_le : ulp n a ≤ 2 * b
hfe : round (a - round (a - b)) = a - round (a - b)
h₀ : b < round (a - round (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
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
ulp_le : ulp n a ≤ 2 * b
hfe : round (a - round (a - b)) = a - round (a - b)
h₀ : b < round (a - round (a - b))
⊢ trunc n (a - b - round (a - b)) = a - b - round (a - b)
Tactic:
apply trunc_eq_of_round_eq npos hfaithful₁
State after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
ulp_le : ulp n a ≤ 2 * b
hfe : round (a - round (a - b)) = a - round (a - b)
h₀ : b < round (a - round (a - b))
⊢ round (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
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
ulp_le : ulp n a ≤ 2 * b
hfe : round (a - round (a - b)) = a - round (a - b)
h₀ : b < round (a - round (a - b))
⊢ round (a - b - round (a - b)) = a - b - round (a - b)
Tactic:
rewrite [tsub_right_comm, ← hfe]
State after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
ulp_le : ulp n a ≤ 2 * b
hfe : round (a - round (a - b)) = a - round (a - b)
h₀ : b < round (a - round (a - b))
⊢ round (round (a - round (a - b)) - b) = round (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
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
ulp_le : ulp n a ≤ 2 * b
hfe : round (a - round (a - b)) = a - round (a - b)
h₀ : b < round (a - round (a - b))
⊢ round (round (a - round (a - b)) - b) = round (a - round (a - b)) - b
Tactic:
apply round_eq_of_trunc_eq npos hfaithful₀
State after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
ulp_le : ulp n a ≤ 2 * b
hfe : round (a - round (a - b)) = a - round (a - b)
h₀ : b < round (a - round (a - b))
⊢ trunc n (round (a - round (a - b)) - b) = round (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
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
ulp_le : ulp n a ≤ 2 * b
hfe : round (a - round (a - b)) = a - round (a - b)
h₀ : b < round (a - round (a - b))
⊢ trunc n (round (a - round (a - b)) - b) = round (a - round (a - b)) - b
Tactic:
apply s₃ npos hfaithful₀ hfaithful₁ hfa hfb hfb hba le_rfl ulp_le h₀ h₀.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
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
ulp_le : ulp n a ≤ 2 * b
⊢ round (a - round (a - b)) = a - round (a - b)
Tactic:
apply round_eq_of_trunc_eq npos hfaithful₀
State after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
ulp_le : ulp n a ≤ 2 * b
⊢ trunc n (a - round (a - b)) = a - 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
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
ulp_le : ulp n a ≤ 2 * b
⊢ trunc n (a - round (a - b)) = a - round (a - b)
Tactic:
apply s₂ npos hfaithful₀ hfaithful₁ hfa hfb hba
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
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
ulp_le : ulp n a ≤ 2 * b
hfe : round (a - round (a - b)) = a - round (a - b)
⊢ b < round (a - round (a - b))
Tactic:
rewrite [hfe]
State after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
ulp_le : ulp n a ≤ 2 * b
hfe : round (a - round (a - b)) = a - round (a - b)
⊢ b < a - 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
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
ulp_le : ulp n a ≤ 2 * b
hfe : round (a - round (a - b)) = a - round (a - b)
⊢ b < a - round (a - b)
Tactic:
rewrite [lt_tsub_comm]
State after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
ulp_le : ulp n a ≤ 2 * b
hfe : round (a - round (a - b)) = a - 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
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
ulp_le : ulp n a ≤ 2 * b
hfe : round (a - round (a - b)) = a - round (a - b)
⊢ round (a - b) < a - b
Tactic:
exact round_lt
State after:
no goals