law lt_succ_iff_sym

bend-mathlib@0.8.1.0 · nat.bend:4581

import Base

4581# Below a successor means at most: m < n + 1 tests as m <= n, reversed to rewrite toward the simple side.
4582law lt_succ_iff_sym:
4583  for m: Nat
4584  for n: Nat
4585  {Nat.is_le(m, n) == Nat.is_lt(m, 1n+n) : Bool}