law lt_of_le_of_lt
import bend-mathlib@0.8.1.0/nat.bend as Natimport Base
1462# A <= b and b < c imply a < c.
1463law lt_of_le_of_lt:
1464 for a: Nat
1465 for b: Nat
1466 for c: Nat
1467 for ab: le(a, b)
1468 for bc: lt(b, c)
1469 lt(a, c)
import bend-mathlib@0.8.1.0/nat.bend as Natimport Base
1462# A <= b and b < c imply a < c.
1463law lt_of_le_of_lt:
1464 for a: Nat
1465 for b: Nat
1466 for c: Nat
1467 for ab: le(a, b)
1468 for bc: lt(b, c)
1469 lt(a, c)