law nat_le_trans

lawful-words@0.1.0.0 · LAWS.bend:546

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

546law nat_le_trans:
547  for a: Nat
548  for b: Nat
549  for c: Nat
550  for h1: {Nat.is_le(a, b) == True{} : Bool}
551  for h2: {Nat.is_le(b, c) == True{} : Bool}
552  {Nat.is_le(a, c) == True{} : Bool}

Uses (4)

Used by (0)

No other definition uses this definition.