law to_nat_sub_le

lawful-words@0.1.0.0 · proof_u32.bend:605

import Base

605law to_nat_sub_le:
606  for +a: U32
607  for +b: U32
608  for +h: {U32.is_le(b, a) == True{} : Bool}
609  {U32.to_nat(U32.sub(a, b)) == Nat.sub(U32.to_nat(a), U32.to_nat(b)) : Nat}