law le_ft

lawful-bytes@0.1.1.0 · proof_find.bend:322

import Base

322# from <= to as numbers.
323law le_ft:
324  for +from: U32
325  for +to: U32
326  for +hft: {U32.is_le(from, to) == True{} : Bool}
327  {Nat.is_le(U32.to_nat(from), U32.to_nat(to)) == True{} : Bool}