Theorem: sum_and_error₂_lo (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
⊢ round (a - b) + round (round (a - round (a - b)) - b) = a - b
Tactic:
have ⟨hfr₁, _⟩ := b₁ npos hfaithful₀ hfaithful₁ hcorrect₀ hfa hfb hba
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
hfr₁ : trunc n (a - b - round (a - b)) = a - b - round (a - b)
right✝ : trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
⊢ round (a - b) + round (round (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
hfr₁ : trunc n (a - b - round (a - b)) = a - b - round (a - b)
right✝ : trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
⊢ round (a - b) + round (round (a - round (a - b)) - b) = a - b
Tactic:
have hfe : round (a - round (a - b)) = a - round (a - b) := by
  apply round_eq_of_trunc_eq npos hfaithful₀
  exact s₂ npos hfaithful₀ hfaithful₁ hfa hfb hba
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
hfr₁ : trunc n (a - b - round (a - b)) = a - b - round (a - b)
right✝ : trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
hfe : round (a - round (a - b)) = a - round (a - b)
⊢ round (a - b) + round (round (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
hfr₁ : trunc n (a - b - round (a - b)) = a - b - round (a - b)
right✝ : trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
hfe : round (a - round (a - b)) = a - round (a - b)
⊢ round (a - b) + round (round (a - round (a - b)) - b) = a - b
Tactic:
have hfr : round (a - b - round (a - b)) = a - b - round (a - b) :=
  round_eq_of_trunc_eq npos hfaithful₀ $ hfr₁
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
hfr₁ : trunc n (a - b - round (a - b)) = a - b - round (a - b)
right✝ : trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
hfe : round (a - round (a - b)) = a - round (a - b)
hfr : round (a - b - round (a - b)) = a - b - round (a - b)
⊢ round (a - b) + round (round (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
hfr₁ : trunc n (a - b - round (a - b)) = a - b - round (a - b)
right✝ : trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
hfe : round (a - round (a - b)) = a - round (a - b)
hfr : round (a - b - round (a - b)) = a - b - round (a - b)
⊢ round (a - b) + round (round (a - round (a - b)) - b) = a - b
Tactic:
rewrite [hfe]
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
hfr₁ : trunc n (a - b - round (a - b)) = a - b - round (a - b)
right✝ : trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
hfe : round (a - round (a - b)) = a - round (a - b)
hfr : round (a - b - round (a - b)) = a - b - round (a - b)
⊢ round (a - b) + round (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
hfr₁ : trunc n (a - b - round (a - b)) = a - b - round (a - b)
right✝ : trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
hfe : round (a - round (a - b)) = a - round (a - b)
hfr : round (a - b - round (a - b)) = a - b - round (a - b)
⊢ round (a - b) + round (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
hfr₁ : trunc n (a - b - round (a - b)) = a - b - round (a - b)
right✝ : trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
hfe : round (a - round (a - b)) = a - round (a - b)
hfr : round (a - b - round (a - b)) = a - b - round (a - b)
⊢ round (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
hfr₁ : trunc n (a - b - round (a - b)) = a - b - round (a - b)
right✝ : trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
hfe : round (a - round (a - b)) = a - round (a - b)
hfr : round (a - b - round (a - b)) = a - b - round (a - b)
⊢ round (a - b) + round (a - b - round (a - b)) = a - b
Tactic:
rewrite [hfr]
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
hfr₁ : trunc n (a - b - round (a - b)) = a - b - round (a - b)
right✝ : trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
hfe : round (a - round (a - b)) = a - round (a - b)
hfr : round (a - b - round (a - b)) = a - b - round (a - 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
hfr₁ : trunc n (a - b - round (a - b)) = a - b - round (a - b)
right✝ : trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
hfe : round (a - round (a - b)) = a - round (a - b)
hfr : round (a - b - round (a - b)) = a - b - round (a - b)
⊢ round (a - b) + (a - b - round (a - 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
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
hfr₁ : trunc n (a - b - round (a - b)) = a - b - round (a - b)
right✝ : trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
hfe : round (a - round (a - b)) = a - round (a - b)
hfr : round (a - b - round (a - b)) = a - b - round (a - b)
⊢ 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
hfr₁ : trunc n (a - b - round (a - b)) = a - b - round (a - b)
right✝ : trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
hfe : round (a - round (a - b)) = a - round (a - b)
hfr : round (a - b - round (a - b)) = a - b - round (a - b)
⊢ a - b - round (a - b) + round (a - b) = a - b
Tactic:
exact tsub_add_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
hfr₁ : trunc n (a - b - round (a - b)) = a - b - round (a - b)
right✝ : trunc n (round (a - b) - (a - b)) = round (a - b) - (a - 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
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
hfr₁ : trunc n (a - b - round (a - b)) = a - b - round (a - b)
right✝ : trunc n (round (a - b) - (a - b)) = round (a - b) - (a - 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
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
hfr₁ : trunc n (a - b - round (a - b)) = a - b - round (a - b)
right✝ : trunc n (round (a - b) - (a - b)) = round (a - b) - (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