def beyond

bend-collections-laws-math@1.0.0.0 · proofs/math/number/fixprime.bend:174

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/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW

174def beyond(+one: Nat, +h1: {one == 1n : Nat}, +t: Nat, +q: Nat, +hS: {Nat.is_le(C.shift(32n, one), t) == True{} : Bool}, +hq: {Nat.is_le(t, q) == True{} : Bool}, +hqf: {C.fits(32n, q) == True{} : Bool}) -> Empty:
175  L.true_false(Equal.trans(Bool, True{}, Nat.is_le(C.shift(32n, one), q), False{}, Equal.sym(Bool, Nat.is_le(C.shift(32n, one), q), True{}, N.le_trans(C.shift(32n, one), t, q, hS, hq)), N.lt_not_le(q, C.shift(32n, one), WW.lt_one(32n, one, h1, q, hqf))))