Theorem: round_add_le (Fl/Round.lean)

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

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

State before:
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : b ≤ a
⊢ round (2 ^ 1 * a - (a - b)) ≤ 2 ^ 1 * a
Tactic:
apply round_sub_le npos hfaithful₀ hfaithful₁
State after:
case hfa
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : b ≤ a
⊢ trunc n (2 ^ 1 * a) = 2 ^ 1 * a

State before:
case hfa
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : b ≤ a
⊢ trunc n (2 ^ 1 * a) = 2 ^ 1 * a
Tactic:
rw [trunc_pow_mul npos, hfa]
State after:
no goals