law nat_lt_trans

bend-osdev-u32@0.1.0.0 · LAWS_order.bend:17

import Base

17law nat_lt_trans:
18  for +x: Nat
19  for +y: Nat
20  for +z: Nat
21  for h1: {Nat.is_lt(x, y) == True{} : Bool}
22  for h2: {Nat.is_lt(y, z) == True{} : Bool}
23  {Nat.is_lt(x, z) == True{} : Bool}