def fold_lt2_z

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/reduce.bend:121

import Base
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/semiring.bend as SR

121# the hi = 0 case: the fold is lo
122def fold_lt2_z(+t: Nat, +lo: Nat, +cv: Nat, +f: Nat, +ll: {Nat.is_lt(lo, t) == True{} : Bool}, +ef: {f == Nat.add(lo, Nat.mul(0n, cv)) : Nat}) -> {Nat.is_lt(f, t) == True{} : Bool}:
123  %Equal.sym(Nat, f, Nat.add(lo, Nat.mul(0n, cv)), ef) : {Nat.is_lt(_, t) == True{} : Bool}
124  %Equal.sym(Nat, Nat.mul(0n, cv), 0n, SR.zero_mul(cv)) : {Nat.is_lt(Nat.add(lo, _), t) == True{} : Bool}
125  %Equal.sym(Nat, Nat.add(lo, 0n), lo, NA.add_zero(lo)) : {Nat.is_lt(_, t) == True{} : Bool}
126  ll