def hz

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/listops.bend:179

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/ineq.bend as I

179def hz(+lo: Nat, hi: Nat, +t: Nat, +hl: {Nat.is_lt(lo, t) == True{} : Bool}) -> {Nat.is_eq(hi, 0n) == Nat.is_lt(Nat.add(lo, Nat.mul(hi, t)), t) : Bool}:
180  match hi:
181    case 0n:
182      %Equal.sym(Nat, Nat.add(lo, 0n), lo, NA.add_zero(lo)) : {True{} == Nat.is_lt(_, t) : Bool}
183      Equal.sym(Bool, Nat.is_lt(lo, t), True{}, hl)
184    case 1n+ +k:
185      Equal.sym(Bool, Nat.is_lt(Nat.add(lo, Nat.add(t, Nat.mul(k, t))), t), False{}, N.le_not_lt(Nat.add(lo, Nat.add(t, Nat.mul(k, t))), t, N.le_trans(t, Nat.add(t, Nat.mul(k, t)), Nat.add(lo, Nat.add(t, Nat.mul(k, t))), N.le_add_right(t, Nat.mul(k, t)), I.le_add_l(lo, Nat.add(t, Nat.mul(k, t))))))