law le_and_le_sub_iff_add_le

bend-mathlib@0.8.1.0 · nat.bend:1541

import Base

1541# A sum is at most c exactly when a <= c and b <= c - a: a + b <= c tests as both.
1542law le_and_le_sub_iff_add_le:
1543  for a: Nat
1544  for -b: Nat
1545  for c: Nat
1546  {Bool.and(Nat.is_le(a, c), Nat.is_le(b, Nat.sub(c, a))) == Nat.is_le(Nat.add(a, b), c) : Bool}