def sfin_flip

bend-kit-collections@0.1.4.1 · PROOF.bend:4052

import Base
import bend-kit-collections@0.1.4.1/LAWS.bend as Laws
import bend-kit-collections@0.1.4.1/order.bend as Order

4052def sfin_flip(c: Cmp, -r: Cmp) -> {Order.string.fin(Laws.flip(c), Laws.flip(r)) == Laws.flip(Order.string.fin(c, r)) : Cmp}:
4053  match c:
4054    case LT{}:
4055      {==}
4056    case EQ{}:
4057      {==}
4058    case GT{}:
4059      {==}