law lt_succ_iff

lawful-words@0.1.0.0 · proof_nat.bend:645

import Base

645# a < 1 + b is a <= b.
646law lt_succ_iff:
647  for +a: Nat
648  for +b: Nat
649  {Nat.is_lt(a, 1n+b) == Nat.is_le(a, b) : Bool}