law nat_lt_le_trans

lawful-words@0.1.0.0 · LAWS.bend:538

import lawful-words@0.1.0.0/LAWS.bend as LAWS
import Base

538law nat_lt_le_trans:
539  for a: Nat
540  for b: Nat
541  for c: Nat
542  for h1: {Nat.is_lt(a, b) == True{} : Bool}
543  for h2: {Nat.is_le(b, c) == True{} : Bool}
544  {Nat.is_lt(a, c) == True{} : Bool}

Uses (5)

Used by (0)

No other definition uses this definition.