@[extern "lean_nat_add"]
protected def Nat.not_add : (@& Nat) → (@& Nat) → Nat
  | _, _ => 0