Theorem: Nat.div2_lt (YatimaStdLib/Nat.lean)

State before:
n : Nat
h : n ≠ 0
⊢ n / 2 < n
Tactic:
match n with
| 1   => decide
| 2   => decide
| 3   => decide
| n+4 =>
  rw [div_eq, if_pos]
  refine succ_lt_succ (Nat.lt_trans ?_ (lt_succ_self _))
  exact @div2_lt (n + 2) (by simp_arith)
  simp_arith
State after:
no goals

State before:
n : Nat
h : 1 ≠ 0
⊢ 1 / 2 < 1
Tactic:
decide
State after:
no goals

State before:
n : Nat
h : 2 ≠ 0
⊢ 2 / 2 < 2
Tactic:
decide
State after:
no goals

State before:
n : Nat
h : 3 ≠ 0
⊢ 3 / 2 < 3
Tactic:
decide
State after:
no goals

State before:
n✝ n : Nat
h : n + 4 ≠ 0
⊢ (n + 4) / 2 < n + 4
Tactic:
rw [div_eq, if_pos]
State after:
n✝ n : Nat
h : n + 4 ≠ 0
⊢ (n + 4 - 2) / 2 + 1 < n + 4

case hc
n✝ n : Nat
h : n + 4 ≠ 0
⊢ 0 < 2 ∧ 2 ≤ n + 4

State before:
n✝ n : Nat
h : n + 4 ≠ 0
⊢ (n + 4 - 2) / 2 + 1 < n + 4

case hc
n✝ n : Nat
h : n + 4 ≠ 0
⊢ 0 < 2 ∧ 2 ≤ n + 4
Tactic:
refine succ_lt_succ (Nat.lt_trans ?_ (lt_succ_self _))
State after:
n✝ n : Nat
h : n + 4 ≠ 0
⊢ (n + 4 - 2) / 2 < n + 2

case hc
n✝ n : Nat
h : n + 4 ≠ 0
⊢ 0 < 2 ∧ 2 ≤ n + 4

State before:
n✝ n : Nat
h : n + 4 ≠ 0
⊢ (n + 4 - 2) / 2 < n + 2

case hc
n✝ n : Nat
h : n + 4 ≠ 0
⊢ 0 < 2 ∧ 2 ≤ n + 4
Tactic:
exact @div2_lt (n + 2) (by simp_arith)
State after:
case hc
n✝ n : Nat
h : n + 4 ≠ 0
⊢ 0 < 2 ∧ 2 ≤ n + 4

State before:
case hc
n✝ n : Nat
h : n + 4 ≠ 0
⊢ 0 < 2 ∧ 2 ≤ n + 4
Tactic:
simp_arith
State after:
no goals

State before:
n✝ n : Nat
h : n + 4 ≠ 0
⊢ n + 2 ≠ 0
Tactic:
simp_arith
State after:
no goals