-- Generated by the EML-lang Lean backend
-- Source module: clamp_bounded
-- Source file:   /home/monogate/monogate/forge/examples/clamp_bounded.eml
-- Verified fns:  clamp_unit

import MachLib.EML
import MachLib.Trig
import MachLib.Forge
import MachLib.Linarith
import MachLib.FixedPoint
import MachLib.SignTactic

open MachLib
open MachLib.Real

noncomputable def LO : Real := (-(1 : Real))
noncomputable def HI : Real := (1 : Real)

-- ── clamp_unit ──

noncomputable def clamp_unit (x : Real) : Real :=
  (min (max x LO) HI)

theorem clamp_in_unit_interval (x : Real)
    (h_clamp1 : LO ≤ HI) :
    (((clamp_unit x) >= LO)) ∧ (((clamp_unit x) <= HI)) := by
  unfold clamp_unit
  refine ⟨?_, ?_⟩ <;>
    first
    | (apply lo_le_clamp <;> (first | assumption | mach_positivity))
    | apply clamp_le_hi
    | mach_positivity
    | mach_sign
    | rfl
    | sorry  -- out of reach; left for the prover