Theorem: Nat.half_eq_halfImpl (GMLInit/Data/Nat/Coding/Sum.lean)

State before:
⊢ half = halfImpl
Tactic:
funext n
State after:
case h
n : Nat
⊢ n.half = n.halfImpl

State before:
case h
n : Nat
⊢ n.half = n.halfImpl
Tactic:
induction n using Nat.recTwo with
| zero => rfl
| one => rfl
| step n ih =>
  unfold Nat.half
  rw [halfImpl, Nat.add_div_right, ih]
  nat_is_pos
State after:
no goals

State before:
case h.zero

⊢ half 0 = halfImpl 0
Tactic:
rfl
State after:
no goals

State before:
case h.one

⊢ half 1 = halfImpl 1
Tactic:
rfl
State after:
no goals

State before:
case h.step
n : Nat
ih : n.half = n.halfImpl
⊢ (n + 2).half = (n + 2).halfImpl
Tactic:
unfold Nat.half
State after:
case h.step
n : Nat
ih : n.half = n.halfImpl
⊢ n.half + 1 = (n + 2).halfImpl

State before:
case h.step
n : Nat
ih : n.half = n.halfImpl
⊢ n.half + 1 = (n + 2).halfImpl
Tactic:
rw [halfImpl, Nat.add_div_right, ih]
State after:
case h.step.H
n : Nat
ih : n.half = n.halfImpl
⊢ 0 < 2

State before:
case h.step.H
n : Nat
ih : n.half = n.halfImpl
⊢ 0 < 2
Tactic:
nat_is_pos
State after:
no goals