def sm_ge

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/natfuel.bend:253

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/math/natural/arith.bend as NR
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/inverse.bend as IV
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32half.bend as UH

253def sm_ge(+mp: Nat, +s: Nat, +x: Nat, +hxs: {Nat.is_le(x, s) == True{} : Bool}, +hs: {Nat.is_lt(s, 1n+mp) == True{} : Bool}) -> {Nat.mod(Nat.add(s, Nat.sub(1n+mp, x)), 1n+mp) == Nat.sub(s, x) : Nat}:
254  +d = Nat.sub(s, x)
255  +hxm = N.le_trans(x, s, 1n+mp, hxs, N.lt_le(s, 1n+mp, hs))
256  +es = Equal.sym(Nat, Nat.add(d, x), s, Equal.trans(Nat, Nat.add(d, x), Nat.add(x, d), s, N.add_comm(d, x), N.sub_add(s, x, hxs)))
257  +e1 = Equal.trans(Nat, Nat.add(s, Nat.sub(1n+mp, x)), Nat.add(Nat.add(d, x), Nat.sub(1n+mp, x)), Nat.add(d, 1n+mp), Equal.cong(Nat, Nat, t => Nat.add(t, Nat.sub(1n+mp, x)), s, Nat.add(d, x), es), Equal.trans(Nat, Nat.add(Nat.add(d, x), Nat.sub(1n+mp, x)), Nat.add(d, Nat.add(x, Nat.sub(1n+mp, x))), Nat.add(d, 1n+mp), N.add_assoc(d, x, Nat.sub(1n+mp, x)), Equal.cong(Nat, Nat, t => Nat.add(d, t), Nat.add(x, Nat.sub(1n+mp, x)), 1n+mp, N.sub_add(1n+mp, x, hxm))))
258  +e2 = Equal.trans(Nat, Nat.mod(Nat.add(d, 1n+mp), 1n+mp), Nat.mod(Nat.add(d, Nat.mod(1n+mp, 1n+mp)), 1n+mp), Nat.mod(Nat.add(d, 0n), 1n+mp), Equal.sym(Nat, Nat.mod(Nat.add(d, Nat.mod(1n+mp, 1n+mp)), 1n+mp), Nat.mod(Nat.add(d, 1n+mp), 1n+mp), NR.mod_add_r(mp, d, 1n+mp)), Equal.cong(Nat, Nat, t => Nat.mod(Nat.add(d, t), 1n+mp), Nat.mod(1n+mp, 1n+mp), 0n, IV.mod_self(mp)))
259  +hd = N.le_lt_trans(d, s, 1n+mp, UH.sub_le(s, x), hs)
260  Equal.trans(Nat, Nat.mod(Nat.add(s, Nat.sub(1n+mp, x)), 1n+mp), Nat.mod(Nat.add(d, 1n+mp), 1n+mp), d, Equal.cong(Nat, Nat, t => Nat.mod(t, 1n+mp), Nat.add(s, Nat.sub(1n+mp, x)), Nat.add(d, 1n+mp), e1), Equal.trans(Nat, Nat.mod(Nat.add(d, 1n+mp), 1n+mp), Nat.mod(Nat.add(d, 0n), 1n+mp), d, e2, Equal.trans(Nat, Nat.mod(Nat.add(d, 0n), 1n+mp), Nat.mod(d, 1n+mp), d, Equal.cong(Nat, Nat, t => Nat.mod(t, 1n+mp), Nat.add(d, 0n), d, N.add_zero(d)), mod_small(mp, d, hd))))