def lo_le

bend-collections-laws-math@1.0.0.0 · proofs/math/random/wrappers.bend:110

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/spec/math/w64.bend as SW
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as W
import bend-collections-laws-math@1.0.0.0/src/math/random/rand.bend as R
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N

110def lo_le(-S: Data, r: W.U64 & S) -> {Nat.is_le(U32.to_nat(R.fst(U32, S, R.lo32(S, r))), SW.value(R.fst(W.U64, S, r))) == True{} : Bool}:
111  match r:
112    case Tuple{x, s}:
113      match x:
114        case W.U64{+l, +h}:
115          N.le_add_right(v(l), C.shift(32n, v(h)))