Word.carry_lt: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as Word
Lines 157-170 of bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend&start_line=157&end_line=170

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
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/logic.bend as L
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32alg.bend as A
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/addition_bounds.bend as AB
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/division_bounds.bend as DB

# the carry out of an addition is the wrap-around test sum < x
def carry_lt(+n: Nat, +one: Nat, +h1: {one == 1n : Nat}, +s: Nat, +x: Nat, +y: Nat, +c: Bool, +e: {Nat.add(s, sc(n, S.bit_value(c))) == Nat.add(x, y) : Nat}, +hy: {Nat.is_lt(y, sc(n, one)) == True{} : Bool}) -> {Nat.is_lt(s, x) == c : Bool}:
  match c:
    case False{}:
      +e0 = Equal.trans(Nat, s, Nat.add(s, 0n), Nat.add(x, y), Equal.sym(Nat, Nat.add(s, 0n), s, N.add_zero(s)), L.subst(Nat, z => {Nat.add(s, z) == Nat.add(x, y) : Nat}, sc(n, 0n), 0n, A.sc_zero(n), e))
      %Equal.sym(Nat, s, Nat.add(y, x), Equal.trans(Nat, s, Nat.add(x, y), Nat.add(y, x), e0, N.add_comm(x, y))) : {Nat.is_lt(_, x) == False{} : Bool}
      AB.offset_not_less(x, y)
    case True{}:
      +k = sc(n, 1n)
      +hy1 = lt1(n, one, h1, y, hy)
      +l1 = N.lt_add_left(y, k, x, hy1)
      +l2 = L.subst(Nat, z => {Nat.is_lt(z, Nat.add(x, k)) == True{} : Bool}, Nat.add(x, y), Nat.add(k, s), Equal.trans(Nat, Nat.add(x, y), Nat.add(s, k), Nat.add(k, s), Equal.sym(Nat, Nat.add(s, k), Nat.add(x, y), e), N.add_comm(s, k)), l1)
      +l3 = L.subst(Nat, z => {Nat.is_lt(Nat.add(k, s), z) == True{} : Bool}, Nat.add(x, k), Nat.add(k, x), N.add_comm(x, k), l2)
      Equal.trans(Bool, Nat.is_lt(s, x), Nat.is_lt(Nat.add(k, s), Nat.add(k, x)), True{}, Equal.sym(Bool, Nat.is_lt(Nat.add(k, s), Nat.add(k, x)), Nat.is_lt(s, x), DB.cancel_less(k, s, x)), l3)

Uses (16):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/addition_bounds.bend&name=offset_not_less
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/division_bounds.bend&name=cancel_less
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend&name=bit_value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend&name=subst
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=add_comm
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=add_zero
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=lt_add_left
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32alg.bend&name=sc_zero
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend&name=lt1
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend&name=sc