law sub_le

lawful-words@0.1.0.0 · proof_u32.bend:564

import Base

564law sub_le:
565  for +x: Nat
566  for +y: Nat
567  {Nat.is_le(Nat.sub(x, y), x) == True{} : Bool}