law le_of_lt
import bend-mathlib@0.8.1.0/nat.bend as Natimport Base
520# A strict inequality implies the weak one: a < b implies a <= b.
521law le_of_lt:
522 for a: Nat
523 for b: Nat
524 for h: lt(a, b)
525 le(a, b)
import bend-mathlib@0.8.1.0/nat.bend as Natimport Base
520# A strict inequality implies the weak one: a < b implies a <= b.
521law le_of_lt:
522 for a: Nat
523 for b: Nat
524 for h: lt(a, b)
525 le(a, b)