def lt_sq
bend-collections-laws-math@1.0.0.0 · proofs/math/typed/w64sqrt.bend:75
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sqrt.bend as W64sqrt
import Base
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/lib/u32.bend as U
import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD
75def lt_sq(+one: Nat, +h1: {one == 1n : Nat}, +x: U32, +r: U32, +hb: {Nat.is_lt(v(r), WD.sc(16n, one)) == True{} : Bool}) -> {U32.is_lt(x, U32.mul(r, r)) == Nat.is_lt(v(x), sq(v(r))) : Bool}:
76 L.subst(Nat, z => {U32.is_lt(x, U32.mul(r, r)) == Nat.is_lt(v(x), z) : Bool}, v(U32.mul(r, r)), sq(v(r)), sq_exact(one, h1, r, hb), U.is_lt_nat(x, U32.mul(r, r)))