def min_le

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/w64sqrt.bend:233

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32.bend as U

233def min_le(+e: U32, +m: U32, +c: Bool, +hc: {U32.is_lt(e, m) == c : Bool}) -> {Nat.is_le(v(Bool.pick(U32, c, e, m)), v(m)) == True{} : Bool}:
234  match c:
235    case True{}:
236      N.lt_le(v(e), v(m), Equal.trans(Bool, Nat.is_lt(v(e), v(m)), U32.is_lt(e, m), True{}, Equal.sym(Bool, U32.is_lt(e, m), Nat.is_lt(v(e), v(m)), U.is_lt_nat(e, m)), hc))
237    case False{}:
238      N.le_refl(v(m))