law word_cmp_lt_trans

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

import Base

60law word_cmp_lt_trans:
61  for +n: Nat
62  for +a: Word(n)
63  for +b: Word(n)
64  for +c: Word(n)
65  for h1: {Word.cmp(n, a, b) == LT{} : Cmp}
66  for h2: {Word.cmp(n, b, c) == LT{} : Cmp}
67  {Word.cmp(n, a, c) == LT{} : Cmp}