def mo_of

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

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
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/math/typed/u64laws.bend as LW
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU

208def mo_of(+q: WU.U64, +b: WU.U64, +n: Nat, +hn: {Nat.mul(v(q), v(b)) == n : Nat}, +c: Bool, +hc: {C.fits(64n, n) == c : Bool}) -> {I.u64_is(NM.MulOver{q, b}) == Bool.not(c) : Bool}:
209  +e1 = Equal.trans(Bool, I.u64_is(NM.MulOver{q, b}), Bool.not(C.fits(64n, Nat.mul(v(q), v(b)))), Bool.not(C.fits(64n, n)), LW.tests_mul_over(q, b), Equal.cong(Nat, Bool, t => Bool.not(C.fits(64n, t)), Nat.mul(v(q), v(b)), n, hn))
210  Equal.trans(Bool, I.u64_is(NM.MulOver{q, b}), Bool.not(C.fits(64n, n)), Bool.not(c), e1, Equal.cong(Bool, Bool, t => Bool.not(t), C.fits(64n, n), c, hc))