Theorem: a₁_of_uflow (Fl.lean)

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
uflow : a + b < 2 ^ n
⊢ trunc n (a + b - round (a + b)) = a + b - round (a + b) ∧ trunc n (round (a + b) - (a + b)) = round (a + b) - (a + b)
Tactic:
have k : trunc n (a + b) = a + b := trunc_eq_self_of_uflow uflow
State after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
uflow : a + b < 2 ^ n
k : trunc n (a + b) = a + b
⊢ trunc n (a + b - round (a + b)) = a + b - round (a + b) ∧ trunc n (round (a + b) - (a + b)) = round (a + b) - (a + b)

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
uflow : a + b < 2 ^ n
k : trunc n (a + b) = a + b
⊢ trunc n (a + b - round (a + b)) = a + b - round (a + b) ∧ trunc n (round (a + b) - (a + b)) = round (a + b) - (a + b)
Tactic:
have l : round (a + b) = a + b := round_eq_of_trunc_eq npos hfaithful₀ k
State after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
uflow : a + b < 2 ^ n
k : trunc n (a + b) = a + b
l : round (a + b) = a + b
⊢ trunc n (a + b - round (a + b)) = a + b - round (a + b) ∧ trunc n (round (a + b) - (a + b)) = round (a + b) - (a + b)

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
uflow : a + b < 2 ^ n
k : trunc n (a + b) = a + b
l : round (a + b) = a + b
⊢ trunc n (a + b - round (a + b)) = a + b - round (a + b) ∧ trunc n (round (a + b) - (a + b)) = round (a + b) - (a + b)
Tactic:
rewrite [l, tsub_self]
State after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
uflow : a + b < 2 ^ n
k : trunc n (a + b) = a + b
l : round (a + b) = a + b
⊢ trunc n 0 = 0 ∧ trunc n 0 = 0

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
uflow : a + b < 2 ^ n
k : trunc n (a + b) = a + b
l : round (a + b) = a + b
⊢ trunc n 0 = 0 ∧ trunc n 0 = 0
Tactic:
exact ⟨trunc_zero n, trunc_zero n⟩
State after:
no goals