law le_total_true_sym

bend-mathlib@0.8.1.0 · order.bend:116

import Base

116# Totality as a Bool disjunction, reversed to rewrite toward the simple side.
117law le_total_true_sym:
118  for ~A: Data
119  for ~le: A -> A -> Bool
120  for ~le_total: @x: A -> @y: A -> {Bool.or(le(x, y), le(y, x)) == True{} : Bool}
121  for +a: A
122  for +b: A
123  {True{} == Bool.or(le(a, b), le(b, a)) : Bool}