law le_trans4

bend-mathlib@0.8.1.0 · order.bend:22

import Base

22# A chain of four comparisons composes.
23law le_trans4:
24  for ~A: Data
25  for ~le: A -> A -> Bool
26  for ~le_trans: @x: A -> @y: A -> @z: A -> {le(x, y) == True{} : Bool} -> {le(y, z) == True{} : Bool} -> {le(x, z) == True{} : Bool}
27  for +a: A
28  for +b: A
29  for +c: A
30  for +d: A
31  for +e: A
32  for ab: {le(a, b) == True{} : Bool}
33  for bc: {le(b, c) == True{} : Bool}
34  for cd: {le(c, d) == True{} : Bool}
35  for de: {le(d, e) == True{} : Bool}
36  {le(a, e) == True{} : Bool}