law le_trans3

bend-mathlib@0.8.1.0 · order.bend:5

import Base

5# A chain of three comparisons composes.
6law le_trans3:
7  for ~A: Data
8  for ~le: A -> A -> Bool
9  for ~le_trans: @x: A -> @y: A -> @z: A -> {le(x, y) == True{} : Bool} -> {le(y, z) == True{} : Bool} -> {le(x, z) == True{} : Bool}
10  for +a: A
11  for +b: A
12  for +c: A
13  for +d: A
14  for ab: {le(a, b) == True{} : Bool}
15  for bc: {le(b, c) == True{} : Bool}
16  for cd: {le(c, d) == True{} : Bool}
17  {le(a, d) == True{} : Bool}