def clamp_id

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

import Base

93# x in [lo, hi] is left alone
94def clamp_id(+x: Nat, +lo: Nat, +hi: Nat, +h1: {Nat.is_le(lo, x) == True{} : Bool}, +h2: {Nat.is_le(x, hi) == True{} : Bool}) -> {Nat.min(Nat.max(x, lo), hi) == x : Nat}:
95  %Equal.sym(Nat, Nat.max(x, lo), x, max_eq_l(x, lo, h1)) : {Nat.min(_, hi) == x : Nat}
96  min_eq_l(x, hi, h2)