law le_succ_lt

lawful-words@0.1.0.0 · proof_nat.bend:662

import Base

662# 1 + a <= b is a < b.
663law le_succ_lt:
664  for +a: Nat
665  for +b: Nat
666  {Nat.is_le(1n+a, b) == Nat.is_lt(a, b) : Bool}