case a
motive : Nat → Nat → Sort u
x y : Nat
ind : (x y : Nat) → 0 < y ∧ y ≤ x → motive (x - y) y → motive x y
base : (x y : Nat) → ¬(0 < y ∧ y ≤ x) → motive x y
h : 0 < y ∧ y ≤ x
⊢ 0 < y ∧ y ≤ x
motive : Nat → Nat → Sort u
x y : Nat
ind : (x y : Nat) → 0 < y ∧ y ≤ x → motive (x - y) y → motive x y
base : (x y : Nat) → ¬(0 < y ∧ y ≤ x) → motive x y
h : 0 < y ∧ y ≤ x
⊢ (invImage
        (fun a =>
          PSigma.casesOn a fun x snd => PSigma.casesOn snd fun y snd => PSigma.casesOn snd fun ind snd => sizeOf x)
        instWellFoundedRelation).1
    { fst := x - y, snd := { fst := y, snd := { fst := ind, snd := base } } }
    { fst := x, snd := { fst := y, snd := { fst := ind, snd := base } } }
apply div_rec_lemma
no goals
case a
motive : Nat → Nat → Sort u
x y : Nat
ind : (x y : Nat) → 0 < y ∧ y ≤ x → motive (x - y) y → motive x y
base : (x y : Nat) → ¬(0 < y ∧ y ≤ x) → motive x y
h : 0 < y ∧ y ≤ x
⊢ 0 < y ∧ y ≤ x
assumption