Theorem: round_eq_next_trunc_of_gt (Fl/Round.lean)

State before:
n x : ℕ
round : ℕ → ℕ
hfaithful₁ : faithful₁ n round
h : round x > x
⊢ round x = next n (trunc n x)
Tactic:
cases hfaithful₁ x with
| inl hlo =>
  exfalso
  apply Nat.lt_le_asymm h
  exact hlo ▸ (trunc_le n x)
| inr hhi => exact hhi
State after:
no goals

State before:
case inl
n x : ℕ
round : ℕ → ℕ
hfaithful₁ : faithful₁ n round
h : round x > x
hlo : round x = trunc n x
⊢ round x = next n (trunc n x)
Tactic:
exfalso
State after:
case inl.h
n x : ℕ
round : ℕ → ℕ
hfaithful₁ : faithful₁ n round
h : round x > x
hlo : round x = trunc n x
⊢ False

State before:
case inl.h
n x : ℕ
round : ℕ → ℕ
hfaithful₁ : faithful₁ n round
h : round x > x
hlo : round x = trunc n x
⊢ False
Tactic:
apply Nat.lt_le_asymm h
State after:
case inl.h
n x : ℕ
round : ℕ → ℕ
hfaithful₁ : faithful₁ n round
h : round x > x
hlo : round x = trunc n x
⊢ round x ≤ x

State before:
case inl.h
n x : ℕ
round : ℕ → ℕ
hfaithful₁ : faithful₁ n round
h : round x > x
hlo : round x = trunc n x
⊢ round x ≤ x
Tactic:
exact hlo ▸ (trunc_le n x)
State after:
no goals

State before:
case inr
n x : ℕ
round : ℕ → ℕ
hfaithful₁ : faithful₁ n round
h : round x > x
hhi : round x = next n (trunc n x)
⊢ round x = next n (trunc n x)
Tactic:
exact hhi
State after:
no goals