def w_r

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

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

506def w_r(+q: Nat, +r: Nat, +p: Nat, +hr: {Nat.is_lt(r, 2n) == True{} : Bool}, +hw: {Nat.is_le(Nat.add(Nat.double(q), r), Nat.double(p)) == True{} : Bool}) -> {Nat.is_le(Nat.add(q, r), p) == True{} : Bool}:
507  match r:
508    case 0n:
509      +h0 = L.subst(Nat, z => {Nat.is_le(z, Nat.double(p)) == True{} : Bool}, Nat.add(Nat.double(q), 0n), Nat.double(q), N.add_zero(Nat.double(q)), hw)
510      L.subst(Nat, z => {Nat.is_le(z, p) == True{} : Bool}, q, Nat.add(q, 0n), Equal.sym(Nat, Nat.add(q, 0n), q, N.add_zero(q)), dle(q, p, h0))
511    case 1n:
512      +h0 = L.subst(Nat, z => {Nat.is_le(z, Nat.double(p)) == True{} : Bool}, Nat.add(Nat.double(q), 1n), 1n+Nat.double(q), plus1(Nat.double(q)), hw)
513      +hq = N.bit_double_lt(False{}, q, p, N.succ_le_lt(Nat.double(q), Nat.double(p), h0))
514      L.subst(Nat, z => {Nat.is_le(z, p) == True{} : Bool}, 1n+q, Nat.add(q, 1n), Equal.sym(Nat, Nat.add(q, 1n), 1n+q, plus1(q)), N.lt_succ_le_succ(q, p, hq))
515    case 2n+s:
516      Empty.absurd({Nat.is_le(Nat.add(q, 2n+s), p) == True{} : Bool}, N.lt_zero_absurd(s, hr))