law fit_mono

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/poly1305/value.bend:631

import Base

631law fit_mono:
632  for +xs: List<&2, U32>
633  for +a: Nat
634  for +b: Nat
635  for +hab: {Nat.is_le(a, b) == True{} : Bool}
636  for +h: {fit_all(xs, a) == True{} : Bool}
637  {fit_all(xs, b) == True{} : Bool}