~/jendhub

law lt_of_succ_le

bend-mathlib@0.8.1.0 · nat.bend:2602

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

2602# A weak inequality from the successor gives the strict one: n + 1 <= m implies n < m.
2603law lt_of_succ_le:
2604  for n: Nat
2605  for m: Nat
2606  for h: le(1n+n, m)
2607  lt(n, m)

Uses (8)

Used by (0)

No other definition uses this definition.