law decb_fits_m

lawful-fields@0.1.1.0 · proof_list.bend:452

import Base
import lawful-fields@0.1.1.0/defs.bend as F

452law decb_fits_m:
453  for +xs: List<&2, U32>
454  for +n: Nat
455  for +m: Nat
456  for +h: {F.dec(xs) == Some{n} : Maybe<&2, Nat>}
457  for +hn: {Nat.is_lt(n, m) == True{} : Bool}
458  {F.decb(xs, m) == Some{n} : Maybe<&2, Nat>}