law le_and_le_sub_iff_add_le_sym

bend-mathlib@0.8.1.0 · nat.bend:4311

import Base

4311# A sum is at most c exactly when a <= c and b <= c - a: a + b <= c tests as both, reversed to rewrite toward the simple side.
4312law le_and_le_sub_iff_add_le_sym:
4313  for a: Nat
4314  for -b: Nat
4315  for c: Nat
4316  {Nat.is_le(Nat.add(a, b), c) == Bool.and(Nat.is_le(a, c), Nat.is_le(b, Nat.sub(c, a))) : Bool}