def lt_sq

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

import Base
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/math/typed/natfuel.bend as NF

40# 2 <= d: d < d * d
41def lt_sq(+dq: Nat) -> {Nat.is_lt(2n+dq, Nat.mul(2n+dq, 2n+dq)) == True{} : Bool}:
42  +h1 = NF.dbl_le_mul(2n+dq, dq)
43  +h2 = N.succ_le_lt(2n+dq, Nat.double(2n+dq), N.double_succ_le(2n+dq, {==}))
44  N.lt_le_trans(2n+dq, Nat.double(2n+dq), Nat.mul(2n+dq, 2n+dq), h2, h1)