law lt_succ_iff

bend-mathlib@0.8.1.0 · nat.bend:2543

import Base

2543# Below a successor means at most: m < n + 1 tests as m <= n.
2544law lt_succ_iff:
2545  for m: Nat
2546  for n: Nat
2547  {Nat.is_lt(m, 1n+n) == Nat.is_le(m, n) : Bool}