∀ {k m : ℕ} (motive : (x : ℕ) → k + x < m + x → Prop) (x : ℕ) (x_1 : k + x < m + x),
  (∀ (h : k + 0 < m + 0), motive 0 h) → (∀ (n : ℕ) (h : k + (n + 1) < m + (n + 1)), motive n.succ h) → motive x x_1