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
n : Nat
h : n ≠ 0
⊢ n / 2 < n
no goals