law le_trans

bend-mathlib@0.8.1.0 · nat.bend:408

import Base

408# The order is transitive: a <= b and b <= c imply a <= c.
409law le_trans:
410  for a: Nat
411  for b: Nat
412  for c: Nat
413  for ab: le(a, b)
414  for bc: le(b, c)
415  le(a, c)