Theorem: monotonic (Fl/Round.lean)

State before:
n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
⊢ sub_left_monotonic n round ∧ sub_right_monotonic n round
Tactic:
unfold sub_left_monotonic
State after:
n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
⊢ (∀ {a b c : ℕ}, trunc n a = a → trunc n b = b → trunc n c = c → a ≤ b → round (c - b) ≤ round (c - a)) ∧
    sub_right_monotonic n round

State before:
n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
⊢ (∀ {a b c : ℕ}, trunc n a = a → trunc n b = b → trunc n c = c → a ≤ b → round (c - b) ≤ round (c - a)) ∧
    sub_right_monotonic n round
Tactic:
unfold sub_right_monotonic
State after:
n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
⊢ (∀ {a b c : ℕ}, trunc n a = a → trunc n b = b → trunc n c = c → a ≤ b → round (c - b) ≤ round (c - a)) ∧
    ∀ {a b c : ℕ}, trunc n a = a → trunc n b = b → trunc n c = c → a ≤ b → round (a - c) ≤ round (b - c)

State before:
n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
⊢ (∀ {a b c : ℕ}, trunc n a = a → trunc n b = b → trunc n c = c → a ≤ b → round (c - b) ≤ round (c - a)) ∧
    ∀ {a b c : ℕ}, trunc n a = a → trunc n b = b → trunc n c = c → a ≤ b → round (a - c) ≤ round (b - c)
Tactic:
constructor
State after:
case left
n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
⊢ ∀ {a b c : ℕ}, trunc n a = a → trunc n b = b → trunc n c = c → a ≤ b → round (c - b) ≤ round (c - a)

case right
n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
⊢ ∀ {a b c : ℕ}, trunc n a = a → trunc n b = b → trunc n c = c → a ≤ b → round (a - c) ≤ round (b - c)

State before:
case left
n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
⊢ ∀ {a b c : ℕ}, trunc n a = a → trunc n b = b → trunc n c = c → a ≤ b → round (c - b) ≤ round (c - a)

case right
n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
⊢ ∀ {a b c : ℕ}, trunc n a = a → trunc n b = b → trunc n c = c → a ≤ b → round (a - c) ≤ round (b - c)
Tactic:
.   intro a b c _ _ _ hab
    apply round_le_round npos hfaithful₁ hcorrect₀ hcorrect₁
    exact tsub_le_tsub_left hab _
State after:
case right
n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
⊢ ∀ {a b c : ℕ}, trunc n a = a → trunc n b = b → trunc n c = c → a ≤ b → round (a - c) ≤ round (b - c)

State before:
case right
n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
⊢ ∀ {a b c : ℕ}, trunc n a = a → trunc n b = b → trunc n c = c → a ≤ b → round (a - c) ≤ round (b - c)
Tactic:
.   intro a b c _ _ _ hba
    apply round_le_round npos hfaithful₁ hcorrect₀ hcorrect₁
    exact tsub_le_tsub_right hba _
State after:
no goals

State before:
case left
n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
⊢ ∀ {a b c : ℕ}, trunc n a = a → trunc n b = b → trunc n c = c → a ≤ b → round (c - b) ≤ round (c - a)
Tactic:
intro a b c _ _ _ hab
State after:
case left
n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
a b c : ℕ
a✝² : trunc n a = a
a✝¹ : trunc n b = b
a✝ : trunc n c = c
hab : a ≤ b
⊢ round (c - b) ≤ round (c - a)

State before:
case left
n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
a b c : ℕ
a✝² : trunc n a = a
a✝¹ : trunc n b = b
a✝ : trunc n c = c
hab : a ≤ b
⊢ round (c - b) ≤ round (c - a)
Tactic:
apply round_le_round npos hfaithful₁ hcorrect₀ hcorrect₁
State after:
case left
n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
a b c : ℕ
a✝² : trunc n a = a
a✝¹ : trunc n b = b
a✝ : trunc n c = c
hab : a ≤ b
⊢ c - b ≤ c - a

State before:
case left
n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
a b c : ℕ
a✝² : trunc n a = a
a✝¹ : trunc n b = b
a✝ : trunc n c = c
hab : a ≤ b
⊢ c - b ≤ c - a
Tactic:
exact tsub_le_tsub_left hab _
State after:
no goals

State before:
case right
n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
⊢ ∀ {a b c : ℕ}, trunc n a = a → trunc n b = b → trunc n c = c → a ≤ b → round (a - c) ≤ round (b - c)
Tactic:
intro a b c _ _ _ hba
State after:
case right
n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
a b c : ℕ
a✝² : trunc n a = a
a✝¹ : trunc n b = b
a✝ : trunc n c = c
hba : a ≤ b
⊢ round (a - c) ≤ round (b - c)

State before:
case right
n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
a b c : ℕ
a✝² : trunc n a = a
a✝¹ : trunc n b = b
a✝ : trunc n c = c
hba : a ≤ b
⊢ round (a - c) ≤ round (b - c)
Tactic:
apply round_le_round npos hfaithful₁ hcorrect₀ hcorrect₁
State after:
case right
n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
a b c : ℕ
a✝² : trunc n a = a
a✝¹ : trunc n b = b
a✝ : trunc n c = c
hba : a ≤ b
⊢ a - c ≤ b - c

State before:
case right
n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
a b c : ℕ
a✝² : trunc n a = a
a✝¹ : trunc n b = b
a✝ : trunc n c = c
hba : a ≤ b
⊢ a - c ≤ b - c
Tactic:
exact tsub_le_tsub_right hba _
State after:
no goals