law lt_succ_of_le

bend-mathlib@0.8.1.0 · nat.bend:2582

import bend-mathlib@0.8.1.0/nat.bend as Nat

import Base

2582# At most is below the successor: m <= n implies m < n + 1.
2583law lt_succ_of_le:
2584  for m: Nat
2585  for n: Nat
2586  for h: le(m, n)
2587  lt(m, 1n+n)

Uses (8)

Used by (2)