def qs_spec

bend-collections-laws-math@1.0.0.0 · proofs/math/u64/u64div.bend:364

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

364def qs_spec(+w: Word(64n), +neg: Bool) -> {qs(w, neg, 1000000) == S.quotient_signed(w, neg) : Word(64n)}:
365  match neg:
366    case False{}:
367      {==}
368    case True{}:
369      {==}