Utility functions around Nat.hasNotBit, used by sparse cases.

def mkHasNotBit (e : Lean.Expr) (ns : Array Nat) : Lean.Expr

def mkHasNotBitProof (e : Lean.Expr) (ns : Array Nat) : Lean.MetaM Lean.Expr

def isHasNotBit? (e : Lean.Expr) : Option Lean.Expr

def refutableHasNotBit? (e : Lean.Expr) : Lean.MetaM (Option Lean.Expr)

Is e a hasNotBit type that can be refuted? Then return an expression that's the negation of it. (This is used by contradiction)