law le_of_succ_le_succ

bend-mathlib@0.8.1.0 · nat.bend:1428

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

import Base

1428# The order of successors is the order of the naturals: a + 1 <= b + 1 implies a <= b.
1429law le_of_succ_le_succ:
1430  for -a: Nat
1431  for -b: Nat
1432  for h: le(1n+a, 1n+b)
1433  le(a, b)

Uses (2)

Used by (2)