law succ_le_of_lt

bend-mathlib@0.8.1.0 · nat.bend:2592

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

import Base

2592# A strict inequality gives the weak one from the successor: n < m implies n + 1 <= m.
2593law succ_le_of_lt:
2594  for n: Nat
2595  for m: Nat
2596  for h: lt(n, m)
2597  le(1n+n, m)

Uses (9)

Used by (3)