law lmax

lawful-fields@0.1.1.0 · proof_digits.bend:556

import Base

556law lmax:
557  for +x: Nat
558  for +z: Nat
559  for +M: Nat
560  for +hx: {Nat.is_lt(x, M) == True{} : Bool}
561  for +hz: {z == Nat.sub(Nat.sub(M, 1n), U32.to_nat(0)) : Nat}
562  {Nat.is_le(x, z) == True{} : Bool}