Theorem: Nat.decreasing_induction (Fifteen/Data/Nat/Basic.lean)

State before:
motive : Nat → Prop
succ : ∀ (n : Nat), motive (n + 1) → motive n
m n : Nat
beg : motive n
h : m ≤ n
⊢ motive m
Tactic:
induction h with
| refl => exact beg
| @step n _ IH => exact IH <| succ _ beg
State after:
no goals

State before:
case refl
motive : Nat → Prop
succ : ∀ (n : Nat), motive (n + 1) → motive n
m n : Nat
beg : motive m
⊢ motive m
Tactic:
exact beg
State after:
no goals

State before:
case step
motive : Nat → Prop
succ : ∀ (n : Nat), motive (n + 1) → motive n
m n✝ n : Nat
a✝ : Nat.le m n
IH : motive n → motive m
beg : motive (Nat.succ n)
⊢ motive m
Tactic:
exact IH <| succ _ beg
State after:
no goals