How to get rid of decidable clause in a polymorphic function

Stream: new members

[Colin Jones ⚛️]

There is an error in the if then statement because the 1 le to x is undecidable. How do put that as a requirement to run the function?

def function1 {α : Type} [LE α] [One α] [Zero α] [HMul ℕ α α] (x : α) : α :=
  if 1 ≤ x then
    4 * x
  else
    0

[Edward van de Meent]

[Decidable (1 <= x)]

[Aaron Liu]

Alternatively, [DecidableLE α]