def gtop.go

lawful-bytes@0.1.1.0 · proof_fast_find.bend:401

import Base
import lawful-words@0.1.0.0/proof_nat.bend as N
import lawful-arrays@0.1.0.0/proof_base.bend as AB

401def gtop.go(+tt: Nat, +m: Nat, +ht: {Nat.is_lt(tt, m) == True{} : Bool}) -> {Nat.is_lt(Nat.sub(Nat.sub(m, 1n), 0n), tt) == False{} : Bool}:
402  match m:
403    case 0n:
404      Empty.absurd({Nat.is_lt(0n, tt) == False{} : Bool}, AB.lt_zero_absurd(tt, ht))
405    case 1n+p:
406      %Equal.sym(Nat, Nat.sub(Nat.sub(p, 0n), 0n), Nat.sub(p, 0n), N.sub_zero(Nat.sub(p, 0n))) : {Nat.is_lt(_, tt) == False{} : Bool}
407      %Equal.sym(Nat, Nat.sub(p, 0n), p, N.sub_zero(p)) : {Nat.is_lt(_, tt) == False{} : Bool}
408      N.le_not_lt(tt, p, Equal.trans(Bool, Nat.is_le(tt, p), Nat.is_lt(tt, 1n+p), True{}, Equal.sym(Bool, Nat.is_lt(tt, 1n+p), Nat.is_le(tt, p), N.lt_succ_iff(tt, p)), ht))