obtain ⟨g, rfl⟩ : ∃ g : ℕ → ℕ, f = λ x ↦ (g x.natPred).succPNat :=
  ⟨λ x ↦ (f x.succPNat).natPred,
    funext (λ x ↦ by rw [PNat.succPNat_natPred, PNat.succPNat_natPred])⟩
f : ℕ+ → ℕ+
⊢ ((∀ (x y : ℕ+), f (y + f x - 1) < f y + x) ∧
      (∀ (x y : ℕ+), x < f y + f (y + f x - 1)) ∧ ∀ (x y : ℕ+), f y < f (y + f x - 1) + x) ↔
    f = fun x => x
case intro
g : ℕ → ℕ
⊢ ((∀ (x y : ℕ+),
        (fun x => (g x.natPred).succPNat) (y + (fun x => (g x.natPred).succPNat) x - 1) <
          (fun x => (g x.natPred).succPNat) y + x) ∧
      (∀ (x y : ℕ+),
          x <
            (fun x => (g x.natPred).succPNat) y +
              (fun x => (g x.natPred).succPNat) (y + (fun x => (g x.natPred).succPNat) x - 1)) ∧
        ∀ (x y : ℕ+),
          (fun x => (g x.natPred).succPNat) y <
            (fun x => (g x.natPred).succPNat) (y + (fun x => (g x.natPred).succPNat) x - 1) + x) ↔
    (fun x => (g x.natPred).succPNat) = fun x => x