Reduce.small_one: def of bend-collections-laws-crypto@1.0.0.0 Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/reduce.bend as Reduce Lines 75-95 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/reduce.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/reduce.bend&start_line=75&end_line=95 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/logic.bend as L import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as WD 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/curve25519/num.bend as M import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend as LM import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/poly.bend as PL # case c >= 1: then a < K and c == 1, so a + 38 < K + 38 <= T def small_one(+one: Nat, +h1: {one == 1n : Nat}, +a: Nat, +c: Nat, +V: Nat, +hv: {Nat.add(a, LM.shn(32n, c)) == V : Nat}, +hV: {Nat.is_lt(V, Nat.add(LM.shn(32n, one), WD.sc(27n, one))) == True{} : Bool}, +hc: {Nat.is_le(one, c) == True{} : Bool}) -> {Nat.is_lt(Nat.add(a, Nat.mul(38n, c)), LM.shn(32n, one)) == True{} : Bool}: +T = LM.shn(32n, one) +K = WD.sc(27n, one) +s = LM.shn(32n, c) +hs = shn_ge(one, c, hc) +v1 = L.subst(Nat, z => {Nat.is_lt(z, Nat.add(T, K)) == True{} : Bool}, V, Nat.add(a, s), Equal.sym(Nat, Nat.add(a, s), V, hv), hV) +v2 = N.le_lt_trans(Nat.add(a, T), Nat.add(a, s), Nat.add(T, K), N.le_add_left(T, s, a, hs), v1) +v3 = L.subst(Nat, z => {Nat.is_lt(Nat.add(a, T), z) == True{} : Bool}, Nat.add(T, K), Nat.add(K, T), NA.add_comm(T, K), v2) +ak = lt_cancel_r(a, K, T, v3) +w1 = N.le_lt_trans(s, Nat.add(a, s), Nat.add(T, K), PL.le_add_l(a, s), v1) +w2 = N.lt_le_trans(s, Nat.add(T, K), Nat.add(T, T), w1, N.le_add_left(K, T, T, k_le_t(one, h1))) +w3 = L.subst(Nat, z => {Nat.is_lt(s, z) == True{} : Bool}, Nat.add(T, T), LM.shn(32n, Nat.add(one, one)), M.sc_add(256n, one, one), w2) +c2 = shn_lt_cancel(c, Nat.add(one, one), w3) +c2b = L.subst(Nat, o => {Nat.is_lt(c, Nat.add(o, o)) == True{} : Bool}, one, 1n, h1, c2) +cle = L.subst(Nat, o => {Nat.is_le(c, o) == True{} : Bool}, 1n, one, Equal.sym(Nat, one, 1n, h1), N.lt_succ_le(c, 1n, c2b)) +ce = N.le_antisym(c, one, cle, hc) +m1 = L.subst(Nat, o => {Nat.mul(38n, o) == 38n : Nat}, 1n, one, Equal.sym(Nat, one, 1n, h1), {==}) %Equal.cong(Nat, Nat, z => Nat.add(a, Nat.mul(38n, z)), one, c, Equal.sym(Nat, c, one, ce)) : {Nat.is_lt(_, T) == True{} : Bool} %M.cong_r(a, 38n, Nat.mul(38n, one), Equal.sym(Nat, Nat.mul(38n, one), 38n, m1)) : {Nat.is_lt(_, T) == True{} : Bool} N.lt_le_trans(Nat.add(a, 38n), Nat.add(K, 38n), T, N.lt_add_r2(a, K, 38n, ak), k38_le_t(one, h1)) Uses (26): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym 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_le https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend&name=shn https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend&name=cong_r https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend&name=sc_add https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/poly.bend&name=le_add_l https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/reduce.bend&name=k38_le_t https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/reduce.bend&name=k_le_t https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/reduce.bend&name=lt_cancel_r https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/reduce.bend&name=shn_ge https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/reduce.bend&name=shn_lt_cancel https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_comm 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=le_add_left https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=le_antisym https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=le_lt_trans https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=lt_add_r2 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=lt_le_trans https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=lt_succ_le https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend&name=sc