no goals
motive : Nat → Prop
x y : Nat
h₁ : y ≤ x → ∀ (k : Nat), x = y + k → motive k
h₂ : x < y → motive 0
⊢ motive (x - y)
cases Nat.lt_or_ge x y with
| inl hlt => rw [Nat.sub_eq_zero_of_le (Nat.le_of_lt hlt)]; exact h₂ hlt
| inr hle => exact h₁ hle (x - y) (Nat.add_sub_of_le hle).symm
case inl
motive : Nat → Prop
x y : Nat
h₁ : y ≤ x → ∀ (k : Nat), x = y + k → motive k
h₂ : x < y → motive 0
hlt : x < y
⊢ motive 0
case inl
motive : Nat → Prop
x y : Nat
h₁ : y ≤ x → ∀ (k : Nat), x = y + k → motive k
h₂ : x < y → motive 0
hlt : x < y
⊢ motive (x - y)
rw [Nat.sub_eq_zero_of_le (Nat.le_of_lt hlt)]
no goals
case inl
motive : Nat → Prop
x y : Nat
h₁ : y ≤ x → ∀ (k : Nat), x = y + k → motive k
h₂ : x < y → motive 0
hlt : x < y
⊢ motive 0
exact h₂ hlt
no goals
case inr
motive : Nat → Prop
x y : Nat
h₁ : y ≤ x → ∀ (k : Nat), x = y + k → motive k
h₂ : x < y → motive 0
hle : x ≥ y
⊢ motive (x - y)
exact h₁ hle (x - y) (Nat.add_sub_of_le hle).symm