law le_sub_l

lawful-words@0.1.0.0 · proof_bytes.bend:505

import Base

505law le_sub_l:
506  for +n: Nat
507  for +r: Nat
508  for +j: Nat
509  for +h: {Nat.is_le(n, Nat.add(j, r)) == True{} : Bool}
510  {Nat.is_le(Nat.sub(n, r), j) == True{} : Bool}