Theorem: round_sub_le (Fl/Round.lean)

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

a n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
b : ℕ
hfa : trunc n a = a
⊢ trunc n a ≤ a

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

a n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
b : ℕ
hfa : trunc n a = a
⊢ trunc n a ≤ a
Tactic:
. apply round_le_trunc_of_le_trunc npos hfaithful₀ hfaithful₁
  exact Nat.le_trans tsub_le_self hfa.ge
State after:
a n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
b : ℕ
hfa : trunc n a = a
⊢ trunc n a ≤ a

State before:
a n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
b : ℕ
hfa : trunc n a = a
⊢ trunc n a ≤ a
Tactic:
. exact trunc_le _ _
State after:
no goals

State before:
a n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
b : ℕ
hfa : trunc n a = a
⊢ round (a - b) ≤ trunc n a
Tactic:
apply round_le_trunc_of_le_trunc npos hfaithful₀ hfaithful₁
State after:
a n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
b : ℕ
hfa : trunc n a = a
⊢ a - b ≤ trunc n a

State before:
a n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
b : ℕ
hfa : trunc n a = a
⊢ a - b ≤ trunc n a
Tactic:
exact Nat.le_trans tsub_le_self hfa.ge
State after:
no goals

State before:
a n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
b : ℕ
hfa : trunc n a = a
⊢ trunc n a ≤ a
Tactic:
exact trunc_le _ _
State after:
no goals