simp_rw [pnat_to_nat_prop2, Function.funext_iff, pnat_to_nat_prop, Nat.natPred_succPNat,
         Nat.succPNat_inj, ← Function.funext_iff, succ_pnat_add_succ_pnat, pnat_add_sub_cancel,
         Nat.natPred_succPNat, PNat.lt_add_one_iff, Nat.succPNat_le_succPNat]
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
case intro
g : ℕ → ℕ
⊢ ((∀ (m n : ℕ), g (n + g m) ≤ g n + m) ∧ (∀ (m n : ℕ), m ≤ g n + g (n + g m)) ∧ ∀ (m n : ℕ), g n ≤ g (n + g m) + m) ↔
    (fun a => g a) = fun a => a