law w_sub_le

lawful-arrays@0.1.0.0 · proof_words.bend:34

import Base

34law w_sub_le:
35  for +a: U32
36  for +b: U32
37  for +h: {U32.is_le(b, a) == True{} : Bool}
38  {U32.to_nat(U32.sub(a, b)) == Nat.sub(U32.to_nat(a), U32.to_nat(b)) : Nat}