law le_sub_r

lawful-words@0.1.0.0 · proof_nat.bend:1535

import Base

1535# a + c <= x gives c <= x - a.
1536law le_sub_r:
1537  for +a: Nat
1538  for +c: Nat
1539  for +x: Nat
1540  for +h: {Nat.is_le(Nat.add(a, c), x) == True{} : Bool}
1541  {Nat.is_le(c, Nat.sub(x, a)) == True{} : Bool}