law lt_trans

bend-mathlib@0.8.1.0 · nat.bend:496

import Base

496# The strict order is transitive: a < b and b < c imply a < c.
497law lt_trans:
498  for a: Nat
499  for b: Nat
500  for c: Nat
501  for ab: lt(a, b)
502  for bc: lt(b, c)
503  lt(a, c)