unfold Int.neg
n : Nat
⊢ negSucc n = { neg := Int.neg }.1 (ofNat (Nat.succ n))
n : Nat
⊢ negSucc n =
    {
          neg := fun n =>
            match n with
            | ofNat n => negOfNat n
            | negSucc n => ofNat (Nat.succ n) }.1
      (ofNat (Nat.succ n))