law to_nat_sub_le

lawful-words@0.1.0.0 · LAWS.bend:150

import Base

150law to_nat_sub_le:
151  for a: U32
152  for b: U32
153  for h: {U32.is_le(b, a) == True{} : Bool}
154  {U32.to_nat(U32.sub(a, b)) == Nat.sub(U32.to_nat(a), U32.to_nat(b)) : Nat}