law lt_succ_le

minebender-game@1.0.0.0 · proof_base.bend:559

import Base

559# n < k + 1 gives n <= k.
560law lt_succ_le:
561  for +n: Nat
562  for +k: Nat
563  for e: {Nat.is_lt(n, 1n+k) == True{} : Bool}
564  {Nat.is_le(n, k) == True{} : Bool}