PROOF.sfin_flip: def of bend-kit-collections@0.1.4.1
Import: import bend-kit-collections@0.1.4.1/PROOF.bend as PROOF
Lines 4052-4059 of bend-kit-collections@0.1.4.1/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&start_line=4052&end_line=4059

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

def sfin_flip(c: Cmp, -r: Cmp) -> {Order.string.fin(Laws.flip(c), Laws.flip(r)) == Laws.flip(Order.string.fin(c, r)) : Cmp}:
  match c:
    case LT{}:
      {==}
    case EQ{}:
      {==}
    case GT{}:
      {==}

Uses (3):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Cmp
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=flip
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/order.bend&name=string.fin