def AP.fin_le_tf

bend-osdev-array@0.1.0.1 · PROOF.bend:188

import Base

188def AP.fin_le_tf(c: Cmp) -> {Cmp.is_le(Word.cmp.fin(True{}, False{}, c)) == Cmp.is_lt(c) : Bool}:
189  match c:
190    case LT{}:
191      {==}
192    case EQ{}:
193      {==}
194    case GT{}:
195      {==}