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

[Ruben-VandeVelde]

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