law sub_le

lawful-bytes@0.1.1.0 · proof_shift.bend:302

import Base

302law sub_le:
303  for +a: Nat
304  for +b: Nat
305  {Nat.is_le(Nat.sub(a, b), a) == True{} : Bool}