def quot_lt

bend-collections-laws-math@1.0.0.0 · proofs/lib/arith.bend:92

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L

92# q d + r < 2^k d forces q < 2^k
93def quot_lt(+k: Nat, +one: Nat, +h1: {one == 1n : Nat}, +q: Nat, +d: Nat, +r: Nat, +h: {Nat.is_lt(Nat.add(Nat.mul(q, d), r), sc(k, d)) == True{} : Bool}) -> {Nat.is_lt(q, sc(k, one)) == True{} : Bool}:
94  L.subst(Nat, o => {Nat.is_lt(q, S.scale_binary(k, o)) == True{} : Bool}, 1n, one, Equal.sym(Nat, one, 1n, h1), quot_lt_g(k, q, d, r, Nat.is_lt(q, sc(k, 1n)), {==}, h))