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

Require Import Reals.
Require Import Lra.
Open Scope R_scope.

Definition LO : R := (- 1.0).
Definition HI : R := 1.0.

(* ── clamp_unit ── *)

Definition clamp_unit (x : R) : R :=
  Rmin HI (Rmax LO x).

(* source obligations for clamp_unit: {O1, O2} *)
(*   O1 [dc085450c6de] -> PRESERVED (equivalent)  theorem clamp_in_unit_interval -- the statement is checked for well-formedness; whether it is discharged depends on the proof body *)
(*        build: unconditional -- the theorem STATEMENT is in the artifact unconditionally; whether it is PROVED is a separate axis -- this checker rejects an undischarged theorem unless cheating is explicitly enabled *)
(*   O2 [cb08549e70f4] -> PRESERVED (equivalent)  theorem clamp_in_unit_interval -- the statement is checked for well-formedness; whether it is discharged depends on the proof body *)
(*        build: unconditional -- the theorem STATEMENT is in the artifact unconditionally; whether it is PROVED is a separate axis -- this checker rejects an undischarged theorem unless cheating is explicitly enabled *)
Theorem clamp_in_unit_interval (x : R) :
    (((clamp_unit x) >= LO)) /\ (((clamp_unit x) <= HI)).
Proof.
  unfold clamp_unit.
  (* TODO: prove against MachLib foundations *)
Admitted.