[GOAL]
n : ℕ
h : 0 < n
m : ℕ := n / 2
⊢ m < n
[PROOFSTEP]
apply Nat.div_lt_self h
[GOAL]
n : ℕ
h : 0 < n
m : ℕ := n / 2
⊢ 1 < 2
[PROOFSTEP]
decide
[GOAL]
n : ℕ
⊢ Fin.ofNat 0 ≤ Fin.ofNat __do_lift✝
[PROOFSTEP]
simp [Fin.ofNat, LE.le]
[GOAL]
n : ℕ
⊢ 0 ≤ __do_lift✝ % (n + 1)
[PROOFSTEP]
exact Nat.zero_le _
[GOAL]
⊢ 0 < List.length (String.toList " 0123abcABC:,;`\\/")
[PROOFSTEP]
decide
