law lt_of_lt_of_le

bend-mathlib@0.8.1.0 · nat.bend:1438

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

import Base

1438# A < b and b <= c imply a < c.
1439law lt_of_lt_of_le:
1440  for a: Nat
1441  for b: Nat
1442  for c: Nat
1443  for ab: lt(a, b)
1444  for bc: le(b, c)
1445  lt(a, c)

Uses (5)

Used by (2)