def clamp_ge

bend-collections-laws-math@1.0.0.0 · proofs/math/natural/misc.bend:86

import Base

86# lo <= clamp and clamp <= hi
87def clamp_ge(+x: Nat, +lo: Nat, +hi: Nat, +h: {Nat.is_le(lo, hi) == True{} : Bool}) -> {Nat.is_le(lo, Nat.min(Nat.max(x, lo), hi)) == True{} : Bool}:
88  le_min(lo, Nat.max(x, lo), hi, le_max_r(x, lo), h)