Order.le_total_of_not_le: law of bend-mathlib@0.8.1.0
Import: import bend-mathlib@0.8.1.0/order.bend as Order
Lines 74-82 of bend-mathlib@0.8.1.0/order.bend: https://jend.leeeet.dev/read.txt?path=bend-mathlib@0.8.1.0/order.bend&start_line=74&end_line=82

import Base

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

Uses (3):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.or
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/order.bend&name=internal_or_of_false_right