def uq.fin_le_tf

bend-osdev-algo@0.1.0.0 · proof_u32.bend:268

import Base

268def uq.fin_le_tf(c: Cmp) -> {Cmp.is_le(Word.cmp.fin(True{}, False{}, c)) == Cmp.is_lt(c) : Bool}:
269  match c:
270    case LT{}:
271      {==}
272    case EQ{}:
273      {==}
274    case GT{}:
275      {==}