simp [Nat.add_comm]
case ofNat.ofNat
n m : Nat
⊢ {
          hAdd := fun a b =>
            {
                  add := fun m n =>
                    match m, n with
                    | ofNat m, ofNat n => ofNat (m + n)
                    | ofNat m, negSucc n => subNatNat m (Nat.succ n)
                    | negSucc m, ofNat n => subNatNat n (Nat.succ m)
                    | negSucc m, negSucc n => negSucc (Nat.succ (m + n)) }.1
              a b }.1
      (ofNat n) (ofNat m) =
    {
          hAdd := fun a b =>
            {
                  add := fun m n =>
                    match m, n with
                    | ofNat m, ofNat n => ofNat (m + n)
                    | ofNat m, negSucc n => subNatNat m (Nat.succ n)
                    | negSucc m, ofNat n => subNatNat n (Nat.succ m)
                    | negSucc m, negSucc n => negSucc (Nat.succ (m + n)) }.1
              a b }.1
      (ofNat m) (ofNat n)
no goals