law le_total_of_not_le

bend-mathlib@0.8.1.0 · order.bend:74

import Base

74# The other side of a total order holds when one side fails.
75law le_total_of_not_le:
76  for ~A: Data
77  for ~le: A -> A -> Bool
78  for ~le_total: @x: A -> @y: A -> {Bool.or(le(x, y), le(y, x)) == True{} : Bool}
79  for +a: A
80  for +b: A
81  for h: {le(a, b) == False{} : Bool}
82  {le(b, a) == True{} : Bool}