def more_v

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u64int.bend:1146

import Base
import bend-collections-laws-math@1.0.0.0/src/math/generic.bend as G
import bend-collections-laws-math@1.0.0.0/src/math/num.bend as NM
import bend-collections-laws-math@1.0.0.0/src/math/instances.bend as I
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natfuel.bend as NF

1146# inc(lo) < lo + w as 1 < w
1147def more_v(+K: Nat, +hK: {K == 64n : Nat}, +lo: WU.U64, +hi: WU.U64, +a: Nat, +w: Nat, +ha: {v(lo) == a : Nat}, +hh: {v(hi) == Nat.add(a, w) : Nat}, +hw: {Nat.is_lt(0n, w) == True{} : Bool}) -> {I.u64_is(NM.Lt{G.inc(~WU.U64, ~I.u64_op, lo), hi}) == Nat.is_lt(1n, w) : Bool}:
1148  +ei = inc_v(K, hK, lo, hi, a, Nat.add(a, w), ha, hh, lt_add_r(a, w, hw))
1149  Equal.trans(Bool, I.u64_is(NM.Lt{G.inc(~WU.U64, ~I.u64_op, lo), hi}), Nat.is_lt(1n+a, Nat.add(a, w)), Nat.is_lt(1n, w), ltv(G.inc(~WU.U64, ~I.u64_op, lo), hi, 1n+a, Nat.add(a, w), ei, hh), L.subst(Nat, z => {Nat.is_lt(z, Nat.add(a, w)) == Nat.is_lt(1n, w) : Bool}, Nat.add(a, 1n), 1n+a, plus1(a), NF.lt_add_cancel(a, 1n, w)))