def last_below

bendtorch-core@0.1.0.0 · src/tensor/signed_PROOF.bend:115

import Base
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith

115# In range, limit - 1 - k is below limit.
116def last_below(+limit: U32, +k: U32, +inside: {U32.is_lt(k, limit) == True{} : Bool}) ->
117  {U32.is_lt(U32.sub(U32.sub(limit, 1), k), limit) == True{} : Bool}:
118  Equal.trans(Bool, U32.is_lt(U32.sub(U32.sub(limit, 1), k), limit), Nat.is_lt(U32.to_nat(U32.sub(U32.sub(limit, 1), k)), U32.to_nat(limit)), True{},
119    Equal.sym(Bool, Nat.is_lt(U32.to_nat(U32.sub(U32.sub(limit, 1), k)), U32.to_nat(limit)), U32.is_lt(U32.sub(U32.sub(limit, 1), k), limit),
120      Arith.u32_lt(U32.sub(U32.sub(limit, 1), k), limit)),
121    Equal.trans(Bool, Nat.is_lt(U32.to_nat(U32.sub(U32.sub(limit, 1), k)), U32.to_nat(limit)),
122      Nat.is_lt(U32.to_nat(U32.sub(U32.sub(limit, 1), k)), Nat.add(U32.to_nat(U32.sub(U32.sub(limit, 1), k)), 1n+U32.to_nat(k))), True{},
123      Equal.cong(Nat, Bool, x => Nat.is_lt(U32.to_nat(U32.sub(U32.sub(limit, 1), k)), x), U32.to_nat(limit),
124        Nat.add(U32.to_nat(U32.sub(U32.sub(limit, 1), k)), 1n+U32.to_nat(k)),
125        Equal.sym(Nat, Nat.add(U32.to_nat(U32.sub(U32.sub(limit, 1), k)), 1n+U32.to_nat(k)), U32.to_nat(limit), last_inside(limit, k, inside))),
126      lt_past(U32.to_nat(U32.sub(U32.sub(limit, 1), k)), U32.to_nat(k))))