def below

bend-collections-laws-math@1.0.0.0 · proofs/math/number/prime.bend:177

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N

177# d * d <= n: d < n
178def below(+n: Nat, +dq: Nat, +hdd: {Nat.is_lt(n, Nat.mul(2n+dq, 2n+dq)) == False{} : Bool}) -> {Nat.is_lt(2n+dq, n) == True{} : Bool}:
179  N.lt_le_trans(2n+dq, Nat.mul(2n+dq, 2n+dq), n, lt_sq(dq), N.not_lt_le(n, Nat.mul(2n+dq, 2n+dq), hdd))