def jn_lt

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64divn.bend:178

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/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as NR

178def jn_lt(+MX: Nat, +yp: Nat, +w: Nat, +P: Nat, +bp: Nat, +hB: {C.shift(w, 1n+yp) == 1n+bp : Nat}) -> {Nat.is_lt(C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+bp) == True{} : Bool}:
179  L.subst(Nat, z => {Nat.is_lt(C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp)), z) == True{} : Bool}, C.shift(w, 1n+yp), 1n+bp, hB, Equal.trans(Bool, Nat.is_lt(C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp)), C.shift(w, 1n+yp)), Nat.is_lt(Nat.mod(C.shift(P, MX), 1n+yp), 1n+yp), True{}, lt_sh(w, Nat.mod(C.shift(P, MX), 1n+yp), 1n+yp), NR.dm_lt(yp, C.shift(P, MX))))