`interval_cases using ..` appears to only support names of hypotheses, not terms

e.g.

import Mathlib.Tactic

example {a : ℕ} (h₁ : a ≠ 0) (h₂ : a ≠ 1) : 2 ≤ a := by
  by_contra hu
  interval_cases using (Nat.zero_le a), hu <;> contradiction

which yields

    interval_cases failed: provided bound '0 ≤ a' cannot be evaluated

This works:

import Mathlib.Tactic

example {a : ℕ} (h₁ : a ≠ 0) (h₂ : a ≠ 1) : 2 ≤ a := by
  by_contra hu
  let this := (Nat.zero_le a)
  interval_cases using this, hu <;> contradiction

Semi-relatedly, it seems like using also doesn't support passing just one bound; one imagines that non-negativity of Nats or hypotheses in the context could be used along with a single explicit bound.

as reported on zulip

Reproduce the two examples with import Mathlib.Tactic, comparing interval_cases using (Nat.zero_le a), hu with the version that binds the term to this. Start at the interval_cases tactic entry point and determine how using arguments are evaluated; done means term bounds and the reported single-bound case behave as intended, with regression coverage.