Issue4967._<_ =
  λ a b →
    case a of
      _ | a >= 0 →
        case b of
          _ | b >= 0 → a < b
          _ → Agda.Builtin.Bool.Bool.false
      _ → case b of
            _ | b >= 0 → Agda.Builtin.Bool.Bool.true
            _ → a < b
Issue4967.check =
  λ a →
    case a of
      _ | a >= 0 → 0 < a
      _ → Agda.Builtin.Bool.Bool.false
