def nw_lo

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64sqn.bend:28

import Base
import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
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/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as NR
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqa.bend as AQ

28# the lower bound: 2 S <= r0 + Q, with S = c + d and r0 = S + d
29def nw_lo(+N: Nat, +S: Nat, +c: Nat, +d: Nat, +rp: Nat, +hS: {S == M.isqrt(N) : Nat}, +hc: {Nat.add(c, d) == S : Nat}, +hr: {Nat.add(S, d) == 1n+rp : Nat}) -> {Nat.is_le(Nat.add(S, S), Nat.add(Nat.add(S, d), Nat.div(N, 1n+rp))) == True{} : Bool}:
30  +e1 = Equal.trans(Nat, Nat.mul(Nat.add(c, d), Nat.add(c, d)), Nat.add(Nat.add(Nat.add(Nat.mul(c, c), Nat.mul(c, d)), Nat.mul(c, d)), Nat.mul(d, d)), Nat.add(Nat.mul(c, Nat.add(Nat.add(c, d), d)), Nat.mul(d, d)), Equal.trans(Nat, Nat.mul(Nat.add(c, d), Nat.add(c, d)), Nat.add(Nat.add(Nat.mul(c, c), Nat.mul(c, d)), Nat.add(Nat.mul(c, d), Nat.mul(d, d))), Nat.add(Nat.add(Nat.add(Nat.mul(c, c), Nat.mul(c, d)), Nat.mul(c, d)), Nat.mul(d, d)), Equal.trans(Nat, Nat.mul(Nat.add(c, d), Nat.add(c, d)), Nat.add(Nat.add(Nat.mul(c, c), Nat.mul(c, d)), Nat.mul(d, Nat.add(c, d))), Nat.add(Nat.add(Nat.mul(c, c), Nat.mul(c, d)), Nat.add(Nat.mul(c, d), Nat.mul(d, d))), Equal.trans(Nat, Nat.mul(Nat.add(c, d), Nat.add(c, d)), Nat.add(Nat.mul(c, Nat.add(c, d)), Nat.mul(d, Nat.add(c, d))), Nat.add(Nat.add(Nat.mul(c, c), Nat.mul(c, d)), Nat.mul(d, Nat.add(c, d))), NA.mul_add_right(c, d, Nat.add(c, d)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.mul(d, Nat.add(c, d))), Nat.mul(c, Nat.add(c, d)), Nat.add(Nat.mul(c, c), Nat.mul(c, d)), NA.mul_add_left(c, c, d))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.mul(c, c), Nat.mul(c, d)), z), Nat.mul(d, Nat.add(c, d)), Nat.add(Nat.mul(c, d), Nat.mul(d, d)), Equal.trans(Nat, Nat.mul(d, Nat.add(c, d)), Nat.add(Nat.mul(d, c), Nat.mul(d, d)), Nat.add(Nat.mul(c, d), Nat.mul(d, d)), NA.mul_add_left(d, c, d), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.mul(d, d)), Nat.mul(d, c), Nat.mul(c, d), NA.mul_comm(d, c))))), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(c, c), Nat.mul(c, d)), Nat.add(Nat.mul(c, d), Nat.mul(d, d))), Nat.add(Nat.mul(c, c), Nat.add(Nat.mul(c, d), Nat.add(Nat.mul(c, d), Nat.add(Nat.mul(d, d), 0n)))), Nat.add(Nat.add(Nat.add(Nat.mul(c, c), Nat.mul(c, d)), Nat.mul(c, d)), Nat.mul(d, d)), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(c, c), Nat.mul(c, d)), Nat.add(Nat.mul(c, d), Nat.mul(d, d))), Nat.add(Nat.add(Nat.mul(c, c), Nat.add(Nat.mul(c, d), 0n)), Nat.add(Nat.mul(c, d), Nat.add(Nat.mul(d, d), 0n))), Nat.add(Nat.mul(c, c), Nat.add(Nat.mul(c, d), Nat.add(Nat.mul(c, d), Nat.add(Nat.mul(d, d), 0n)))), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(c, c), Nat.mul(c, d)), Nat.add(Nat.mul(c, d), Nat.mul(d, d))), Nat.add(Nat.add(Nat.mul(c, c), Nat.add(Nat.mul(c, d), 0n)), Nat.add(Nat.mul(c, d), Nat.mul(d, d))), Nat.add(Nat.add(Nat.mul(c, c), Nat.add(Nat.mul(c, d), 0n)), Nat.add(Nat.mul(c, d), Nat.add(Nat.mul(d, d), 0n))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(Nat.mul(c, d), Nat.mul(d, d))), Nat.add(Nat.mul(c, c), Nat.mul(c, d)), Nat.add(Nat.mul(c, c), Nat.add(Nat.mul(c, d), 0n)), Equal.trans(Nat, Nat.add(Nat.mul(c, c), Nat.mul(c, d)), Nat.add(Nat.add(Nat.mul(c, c), 0n), Nat.add(Nat.mul(c, d), 0n)), Nat.add(Nat.mul(c, c), Nat.add(Nat.mul(c, d), 0n)), Equal.trans(Nat, Nat.add(Nat.mul(c, c), Nat.mul(c, d)), Nat.add(Nat.add(Nat.mul(c, c), 0n), Nat.mul(c, d)), Nat.add(Nat.add(Nat.mul(c, c), 0n), Nat.add(Nat.mul(c, d), 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.mul(c, d)), Nat.mul(c, c), Nat.add(Nat.mul(c, c), 0n), Equal.sym(Nat, Nat.add(Nat.mul(c, c), 0n), Nat.mul(c, c), N.add_zero(Nat.mul(c, c)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.mul(c, c), 0n), z), Nat.mul(c, d), Nat.add(Nat.mul(c, d), 0n), Equal.sym(Nat, Nat.add(Nat.mul(c, d), 0n), Nat.mul(c, d), N.add_zero(Nat.mul(c, d))))), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(c, c), 0n), Nat.add(Nat.mul(c, d), 0n)), Nat.add(Nat.mul(c, c), Nat.add(0n, Nat.add(Nat.mul(c, d), 0n))), Nat.add(Nat.mul(c, c), Nat.add(Nat.mul(c, d), 0n)), NA.add_assoc(Nat.mul(c, c), 0n, Nat.add(Nat.mul(c, d), 0n)), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(c, c), z), Nat.add(0n, Nat.add(Nat.mul(c, d), 0n)), Nat.add(Nat.mul(c, d), 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(Nat.mul(c, d), 0n)), Nat.add(Nat.mul(c, d), Nat.add(0n, 0n)), Nat.add(Nat.mul(c, d), 0n), NA.add_swap(0n, Nat.mul(c, d), 0n), {==}))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.mul(c, c), Nat.add(Nat.mul(c, d), 0n)), z), Nat.add(Nat.mul(c, d), Nat.mul(d, d)), Nat.add(Nat.mul(c, d), Nat.add(Nat.mul(d, d), 0n)), Equal.trans(Nat, Nat.add(Nat.mul(c, d), Nat.mul(d, d)), Nat.add(Nat.add(Nat.mul(c, d), 0n), Nat.add(Nat.mul(d, d), 0n)), Nat.add(Nat.mul(c, d), Nat.add(Nat.mul(d, d), 0n)), Equal.trans(Nat, Nat.add(Nat.mul(c, d), Nat.mul(d, d)), Nat.add(Nat.add(Nat.mul(c, d), 0n), Nat.mul(d, d)), Nat.add(Nat.add(Nat.mul(c, d), 0n), Nat.add(Nat.mul(d, d), 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.mul(d, d)), Nat.mul(c, d), Nat.add(Nat.mul(c, d), 0n), Equal.sym(Nat, Nat.add(Nat.mul(c, d), 0n), Nat.mul(c, d), N.add_zero(Nat.mul(c, d)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.mul(c, d), 0n), z), Nat.mul(d, d), Nat.add(Nat.mul(d, d), 0n), Equal.sym(Nat, Nat.add(Nat.mul(d, d), 0n), Nat.mul(d, d), N.add_zero(Nat.mul(d, d))))), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(c, d), 0n), Nat.add(Nat.mul(d, d), 0n)), Nat.add(Nat.mul(c, d), Nat.add(0n, Nat.add(Nat.mul(d, d), 0n))), Nat.add(Nat.mul(c, d), Nat.add(Nat.mul(d, d), 0n)), NA.add_assoc(Nat.mul(c, d), 0n, Nat.add(Nat.mul(d, d), 0n)), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(c, d), z), Nat.add(0n, Nat.add(Nat.mul(d, d), 0n)), Nat.add(Nat.mul(d, d), 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(Nat.mul(d, d), 0n)), Nat.add(Nat.mul(d, d), Nat.add(0n, 0n)), Nat.add(Nat.mul(d, d), 0n), NA.add_swap(0n, Nat.mul(d, d), 0n), {==})))))), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(c, c), Nat.add(Nat.mul(c, d), 0n)), Nat.add(Nat.mul(c, d), Nat.add(Nat.mul(d, d), 0n))), Nat.add(Nat.mul(c, c), Nat.add(Nat.add(Nat.mul(c, d), 0n), Nat.add(Nat.mul(c, d), Nat.add(Nat.mul(d, d), 0n)))), Nat.add(Nat.mul(c, c), Nat.add(Nat.mul(c, d), Nat.add(Nat.mul(c, d), Nat.add(Nat.mul(d, d), 0n)))), NA.add_assoc(Nat.mul(c, c), Nat.add(Nat.mul(c, d), 0n), Nat.add(Nat.mul(c, d), Nat.add(Nat.mul(d, d), 0n))), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(c, c), z), Nat.add(Nat.add(Nat.mul(c, d), 0n), Nat.add(Nat.mul(c, d), Nat.add(Nat.mul(d, d), 0n))), Nat.add(Nat.mul(c, d), Nat.add(Nat.mul(c, d), Nat.add(Nat.mul(d, d), 0n))), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(c, d), 0n), Nat.add(Nat.mul(c, d), Nat.add(Nat.mul(d, d), 0n))), Nat.add(Nat.mul(c, d), Nat.add(0n, Nat.add(Nat.mul(c, d), Nat.add(Nat.mul(d, d), 0n)))), Nat.add(Nat.mul(c, d), Nat.add(Nat.mul(c, d), Nat.add(Nat.mul(d, d), 0n))), NA.add_assoc(Nat.mul(c, d), 0n, Nat.add(Nat.mul(c, d), Nat.add(Nat.mul(d, d), 0n))), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(c, d), z), Nat.add(0n, Nat.add(Nat.mul(c, d), Nat.add(Nat.mul(d, d), 0n))), Nat.add(Nat.mul(c, d), Nat.add(Nat.mul(d, d), 0n)), Equal.trans(Nat, Nat.add(0n, Nat.add(Nat.mul(c, d), Nat.add(Nat.mul(d, d), 0n))), Nat.add(Nat.mul(c, d), Nat.add(0n, Nat.add(Nat.mul(d, d), 0n))), Nat.add(Nat.mul(c, d), Nat.add(Nat.mul(d, d), 0n)), NA.add_swap(0n, Nat.mul(c, d), Nat.add(Nat.mul(d, d), 0n)), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(c, d), z), Nat.add(0n, Nat.add(Nat.mul(d, d), 0n)), Nat.add(Nat.mul(d, d), 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(Nat.mul(d, d), 0n)), Nat.add(Nat.mul(d, d), Nat.add(0n, 0n)), Nat.add(Nat.mul(d, d), 0n), NA.add_swap(0n, Nat.mul(d, d), 0n), {==})))))))), Equal.sym(Nat, Nat.add(Nat.add(Nat.add(Nat.mul(c, c), Nat.mul(c, d)), Nat.mul(c, d)), Nat.mul(d, d)), Nat.add(Nat.mul(c, c), Nat.add(Nat.mul(c, d), Nat.add(Nat.mul(c, d), Nat.add(Nat.mul(d, d), 0n)))), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.mul(c, c), Nat.mul(c, d)), Nat.mul(c, d)), Nat.mul(d, d)), Nat.add(Nat.add(Nat.mul(c, c), Nat.add(Nat.mul(c, d), Nat.add(Nat.mul(c, d), 0n))), Nat.add(Nat.mul(d, d), 0n)), Nat.add(Nat.mul(c, c), Nat.add(Nat.mul(c, d), Nat.add(Nat.mul(c, d), Nat.add(Nat.mul(d, d), 0n)))), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.mul(c, c), Nat.mul(c, d)), Nat.mul(c, d)), Nat.mul(d, d)), Nat.add(Nat.add(Nat.mul(c, c), Nat.add(Nat.mul(c, d), Nat.add(Nat.mul(c, d), 0n))), Nat.mul(d, d)), Nat.add(Nat.add(Nat.mul(c, c), Nat.add(Nat.mul(c, d), Nat.add(Nat.mul(c, d), 0n))), Nat.add(Nat.mul(d, d), 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.mul(d, d)), Nat.add(Nat.add(Nat.mul(c, c), Nat.mul(c, d)), Nat.mul(c, d)), Nat.add(Nat.mul(c, c), Nat.add(Nat.mul(c, d), Nat.add(Nat.mul(c, d), 0n))), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(c, c), Nat.mul(c, d)), Nat.mul(c, d)), Nat.add(Nat.add(Nat.mul(c, c), Nat.add(Nat.mul(c, d), 0n)), Nat.add(Nat.mul(c, d), 0n)), Nat.add(Nat.mul(c, c), Nat.add(Nat.mul(c, d), Nat.add(Nat.mul(c, d), 0n))), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(c, c), Nat.mul(c, d)), Nat.mul(c, d)), Nat.add(Nat.add(Nat.mul(c, c), Nat.add(Nat.mul(c, d), 0n)), Nat.mul(c, d)), Nat.add(Nat.add(Nat.mul(c, c), Nat.add(Nat.mul(c, d), 0n)), Nat.add(Nat.mul(c, d), 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.mul(c, d)), Nat.add(Nat.mul(c, c), Nat.mul(c, d)), Nat.add(Nat.mul(c, c), Nat.add(Nat.mul(c, d), 0n)), Equal.trans(Nat, Nat.add(Nat.mul(c, c), Nat.mul(c, d)), Nat.add(Nat.add(Nat.mul(c, c), 0n), Nat.add(Nat.mul(c, d), 0n)), Nat.add(Nat.mul(c, c), Nat.add(Nat.mul(c, d), 0n)), Equal.trans(Nat, Nat.add(Nat.mul(c, c), Nat.mul(c, d)), Nat.add(Nat.add(Nat.mul(c, c), 0n), Nat.mul(c, d)), Nat.add(Nat.add(Nat.mul(c, c), 0n), Nat.add(Nat.mul(c, d), 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.mul(c, d)), Nat.mul(c, c), Nat.add(Nat.mul(c, c), 0n), Equal.sym(Nat, Nat.add(Nat.mul(c, c), 0n), Nat.mul(c, c), N.add_zero(Nat.mul(c, c)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.mul(c, c), 0n), z), Nat.mul(c, d), Nat.add(Nat.mul(c, d), 0n), Equal.sym(Nat, Nat.add(Nat.mul(c, d), 0n), Nat.mul(c, d), N.add_zero(Nat.mul(c, d))))), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(c, c), 0n), Nat.add(Nat.mul(c, d), 0n)), Nat.add(Nat.mul(c, c), Nat.add(0n, Nat.add(Nat.mul(c, d), 0n))), Nat.add(Nat.mul(c, c), Nat.add(Nat.mul(c, d), 0n)), NA.add_assoc(Nat.mul(c, c), 0n, Nat.add(Nat.mul(c, d), 0n)), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(c, c), z), Nat.add(0n, Nat.add(Nat.mul(c, d), 0n)), Nat.add(Nat.mul(c, d), 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(Nat.mul(c, d), 0n)), Nat.add(Nat.mul(c, d), Nat.add(0n, 0n)), Nat.add(Nat.mul(c, d), 0n), NA.add_swap(0n, Nat.mul(c, d), 0n), {==}))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.mul(c, c), Nat.add(Nat.mul(c, d), 0n)), z), Nat.mul(c, d), Nat.add(Nat.mul(c, d), 0n), Equal.sym(Nat, Nat.add(Nat.mul(c, d), 0n), Nat.mul(c, d), N.add_zero(Nat.mul(c, d))))), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(c, c), Nat.add(Nat.mul(c, d), 0n)), Nat.add(Nat.mul(c, d), 0n)), Nat.add(Nat.mul(c, c), Nat.add(Nat.add(Nat.mul(c, d), 0n), Nat.add(Nat.mul(c, d), 0n))), Nat.add(Nat.mul(c, c), Nat.add(Nat.mul(c, d), Nat.add(Nat.mul(c, d), 0n))), NA.add_assoc(Nat.mul(c, c), Nat.add(Nat.mul(c, d), 0n), Nat.add(Nat.mul(c, d), 0n)), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(c, c), z), Nat.add(Nat.add(Nat.mul(c, d), 0n), Nat.add(Nat.mul(c, d), 0n)), Nat.add(Nat.mul(c, d), Nat.add(Nat.mul(c, d), 0n)), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(c, d), 0n), Nat.add(Nat.mul(c, d), 0n)), Nat.add(Nat.mul(c, d), Nat.add(0n, Nat.add(Nat.mul(c, d), 0n))), Nat.add(Nat.mul(c, d), Nat.add(Nat.mul(c, d), 0n)), NA.add_assoc(Nat.mul(c, d), 0n, Nat.add(Nat.mul(c, d), 0n)), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(c, d), z), Nat.add(0n, Nat.add(Nat.mul(c, d), 0n)), Nat.add(Nat.mul(c, d), 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(Nat.mul(c, d), 0n)), Nat.add(Nat.mul(c, d), Nat.add(0n, 0n)), Nat.add(Nat.mul(c, d), 0n), NA.add_swap(0n, Nat.mul(c, d), 0n), {==}))))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.mul(c, c), Nat.add(Nat.mul(c, d), Nat.add(Nat.mul(c, d), 0n))), z), Nat.mul(d, d), Nat.add(Nat.mul(d, d), 0n), Equal.sym(Nat, Nat.add(Nat.mul(d, d), 0n), Nat.mul(d, d), N.add_zero(Nat.mul(d, d))))), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(c, c), Nat.add(Nat.mul(c, d), Nat.add(Nat.mul(c, d), 0n))), Nat.add(Nat.mul(d, d), 0n)), Nat.add(Nat.mul(c, c), Nat.add(Nat.add(Nat.mul(c, d), Nat.add(Nat.mul(c, d), 0n)), Nat.add(Nat.mul(d, d), 0n))), Nat.add(Nat.mul(c, c), Nat.add(Nat.mul(c, d), Nat.add(Nat.mul(c, d), Nat.add(Nat.mul(d, d), 0n)))), NA.add_assoc(Nat.mul(c, c), Nat.add(Nat.mul(c, d), Nat.add(Nat.mul(c, d), 0n)), Nat.add(Nat.mul(d, d), 0n)), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(c, c), z), Nat.add(Nat.add(Nat.mul(c, d), Nat.add(Nat.mul(c, d), 0n)), Nat.add(Nat.mul(d, d), 0n)), Nat.add(Nat.mul(c, d), Nat.add(Nat.mul(c, d), Nat.add(Nat.mul(d, d), 0n))), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(c, d), Nat.add(Nat.mul(c, d), 0n)), Nat.add(Nat.mul(d, d), 0n)), Nat.add(Nat.mul(c, d), Nat.add(Nat.add(Nat.mul(c, d), 0n), Nat.add(Nat.mul(d, d), 0n))), Nat.add(Nat.mul(c, d), Nat.add(Nat.mul(c, d), Nat.add(Nat.mul(d, d), 0n))), NA.add_assoc(Nat.mul(c, d), Nat.add(Nat.mul(c, d), 0n), Nat.add(Nat.mul(d, d), 0n)), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(c, d), z), Nat.add(Nat.add(Nat.mul(c, d), 0n), Nat.add(Nat.mul(d, d), 0n)), Nat.add(Nat.mul(c, d), Nat.add(Nat.mul(d, d), 0n)), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(c, d), 0n), Nat.add(Nat.mul(d, d), 0n)), Nat.add(Nat.mul(c, d), Nat.add(0n, Nat.add(Nat.mul(d, d), 0n))), Nat.add(Nat.mul(c, d), Nat.add(Nat.mul(d, d), 0n)), NA.add_assoc(Nat.mul(c, d), 0n, Nat.add(Nat.mul(d, d), 0n)), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(c, d), z), Nat.add(0n, Nat.add(Nat.mul(d, d), 0n)), Nat.add(Nat.mul(d, d), 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(Nat.mul(d, d), 0n)), Nat.add(Nat.mul(d, d), Nat.add(0n, 0n)), Nat.add(Nat.mul(d, d), 0n), NA.add_swap(0n, Nat.mul(d, d), 0n), {==}))))))))))), Equal.sym(Nat, Nat.add(Nat.mul(c, Nat.add(Nat.add(c, d), d)), Nat.mul(d, d)), Nat.add(Nat.add(Nat.add(Nat.mul(c, c), Nat.mul(c, d)), Nat.mul(c, d)), Nat.mul(d, d)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.mul(d, d)), Nat.mul(c, Nat.add(Nat.add(c, d), d)), Nat.add(Nat.add(Nat.mul(c, c), Nat.mul(c, d)), Nat.mul(c, d)), Equal.trans(Nat, Nat.mul(c, Nat.add(Nat.add(c, d), d)), Nat.add(Nat.mul(c, Nat.add(c, d)), Nat.mul(c, d)), Nat.add(Nat.add(Nat.mul(c, c), Nat.mul(c, d)), Nat.mul(c, d)), NA.mul_add_left(c, Nat.add(c, d), d), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.mul(c, d)), Nat.mul(c, Nat.add(c, d)), Nat.add(Nat.mul(c, c), Nat.mul(c, d)), NA.mul_add_left(c, c, d))))))
31  +l0 = L.subst(Nat, z => {Nat.is_le(Nat.mul(c, Nat.add(Nat.add(c, d), d)), z) == True{} : Bool}, Nat.add(Nat.mul(c, Nat.add(Nat.add(c, d), d)), Nat.mul(d, d)), Nat.mul(Nat.add(c, d), Nat.add(c, d)), Equal.sym(Nat, Nat.mul(Nat.add(c, d), Nat.add(c, d)), Nat.add(Nat.mul(c, Nat.add(Nat.add(c, d), d)), Nat.mul(d, d)), e1), N.le_add_right(Nat.mul(c, Nat.add(Nat.add(c, d), d)), Nat.mul(d, d)))
32  +l1 = L.subst(Nat, z => {Nat.is_le(Nat.mul(c, Nat.add(z, d)), Nat.mul(z, z)) == True{} : Bool}, Nat.add(c, d), S, hc, l0)
33  +l2 = N.le_trans(Nat.mul(c, Nat.add(S, d)), Nat.mul(S, S), N, l1, L.subst(Nat, z => {Nat.is_le(Nat.mul(z, z), N) == True{} : Bool}, M.isqrt(N), S, Equal.sym(Nat, S, M.isqrt(N), hS), AQ.isl(N)))
34  +l3 = L.subst(Nat, z => {Nat.is_le(Nat.mul(c, z), N) == True{} : Bool}, Nat.add(S, d), 1n+rp, hr, l2)
35  +hq = Equal.trans(Bool, Nat.is_le(c, Nat.div(N, 1n+rp)), Nat.is_le(Nat.mul(c, 1n+rp), N), True{}, NR.le_div(rp, c, N), l3)
36  +l4 = N.le_add_left(c, Nat.div(N, 1n+rp), Nat.add(S, d), hq)
37  +e2 = Equal.trans(Nat, Nat.add(Nat.add(S, d), c), Nat.add(S, Nat.add(c, d)), Nat.add(S, S), Equal.trans(Nat, Nat.add(Nat.add(S, d), c), Nat.add(S, Nat.add(c, Nat.add(d, 0n))), Nat.add(S, Nat.add(c, d)), Equal.trans(Nat, Nat.add(Nat.add(S, d), c), Nat.add(Nat.add(S, Nat.add(d, 0n)), Nat.add(c, 0n)), Nat.add(S, Nat.add(c, Nat.add(d, 0n))), Equal.trans(Nat, Nat.add(Nat.add(S, d), c), Nat.add(Nat.add(S, Nat.add(d, 0n)), c), Nat.add(Nat.add(S, Nat.add(d, 0n)), Nat.add(c, 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, c), Nat.add(S, d), Nat.add(S, Nat.add(d, 0n)), Equal.trans(Nat, Nat.add(S, d), Nat.add(Nat.add(S, 0n), Nat.add(d, 0n)), Nat.add(S, Nat.add(d, 0n)), Equal.trans(Nat, Nat.add(S, d), Nat.add(Nat.add(S, 0n), d), Nat.add(Nat.add(S, 0n), Nat.add(d, 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, d), S, Nat.add(S, 0n), Equal.sym(Nat, Nat.add(S, 0n), S, N.add_zero(S))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(S, 0n), z), d, Nat.add(d, 0n), Equal.sym(Nat, Nat.add(d, 0n), d, N.add_zero(d)))), Equal.trans(Nat, Nat.add(Nat.add(S, 0n), Nat.add(d, 0n)), Nat.add(S, Nat.add(0n, Nat.add(d, 0n))), Nat.add(S, Nat.add(d, 0n)), NA.add_assoc(S, 0n, Nat.add(d, 0n)), Equal.cong(Nat, Nat, z => Nat.add(S, z), Nat.add(0n, Nat.add(d, 0n)), Nat.add(d, 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(d, 0n)), Nat.add(d, Nat.add(0n, 0n)), Nat.add(d, 0n), NA.add_swap(0n, d, 0n), {==}))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(S, Nat.add(d, 0n)), z), c, Nat.add(c, 0n), Equal.sym(Nat, Nat.add(c, 0n), c, N.add_zero(c)))), Equal.trans(Nat, Nat.add(Nat.add(S, Nat.add(d, 0n)), Nat.add(c, 0n)), Nat.add(S, Nat.add(Nat.add(d, 0n), Nat.add(c, 0n))), Nat.add(S, Nat.add(c, Nat.add(d, 0n))), NA.add_assoc(S, Nat.add(d, 0n), Nat.add(c, 0n)), Equal.cong(Nat, Nat, z => Nat.add(S, z), Nat.add(Nat.add(d, 0n), Nat.add(c, 0n)), Nat.add(c, Nat.add(d, 0n)), Equal.trans(Nat, Nat.add(Nat.add(d, 0n), Nat.add(c, 0n)), Nat.add(d, Nat.add(c, 0n)), Nat.add(c, Nat.add(d, 0n)), Equal.trans(Nat, Nat.add(Nat.add(d, 0n), Nat.add(c, 0n)), Nat.add(d, Nat.add(0n, Nat.add(c, 0n))), Nat.add(d, Nat.add(c, 0n)), NA.add_assoc(d, 0n, Nat.add(c, 0n)), Equal.cong(Nat, Nat, z => Nat.add(d, z), Nat.add(0n, Nat.add(c, 0n)), Nat.add(c, 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(c, 0n)), Nat.add(c, Nat.add(0n, 0n)), Nat.add(c, 0n), NA.add_swap(0n, c, 0n), {==}))), NA.add_swap(d, c, 0n))))), Equal.sym(Nat, Nat.add(S, Nat.add(c, d)), Nat.add(S, Nat.add(c, Nat.add(d, 0n))), Equal.trans(Nat, Nat.add(S, Nat.add(c, d)), Nat.add(Nat.add(S, 0n), Nat.add(c, Nat.add(d, 0n))), Nat.add(S, Nat.add(c, Nat.add(d, 0n))), Equal.trans(Nat, Nat.add(S, Nat.add(c, d)), Nat.add(Nat.add(S, 0n), Nat.add(c, d)), Nat.add(Nat.add(S, 0n), Nat.add(c, Nat.add(d, 0n))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(c, d)), S, Nat.add(S, 0n), Equal.sym(Nat, Nat.add(S, 0n), S, N.add_zero(S))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(S, 0n), z), Nat.add(c, d), Nat.add(c, Nat.add(d, 0n)), Equal.trans(Nat, Nat.add(c, d), Nat.add(Nat.add(c, 0n), Nat.add(d, 0n)), Nat.add(c, Nat.add(d, 0n)), Equal.trans(Nat, Nat.add(c, d), Nat.add(Nat.add(c, 0n), d), Nat.add(Nat.add(c, 0n), Nat.add(d, 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, d), c, Nat.add(c, 0n), Equal.sym(Nat, Nat.add(c, 0n), c, N.add_zero(c))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(c, 0n), z), d, Nat.add(d, 0n), Equal.sym(Nat, Nat.add(d, 0n), d, N.add_zero(d)))), Equal.trans(Nat, Nat.add(Nat.add(c, 0n), Nat.add(d, 0n)), Nat.add(c, Nat.add(0n, Nat.add(d, 0n))), Nat.add(c, Nat.add(d, 0n)), NA.add_assoc(c, 0n, Nat.add(d, 0n)), Equal.cong(Nat, Nat, z => Nat.add(c, z), Nat.add(0n, Nat.add(d, 0n)), Nat.add(d, 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(d, 0n)), Nat.add(d, Nat.add(0n, 0n)), Nat.add(d, 0n), NA.add_swap(0n, d, 0n), {==})))))), Equal.trans(Nat, Nat.add(Nat.add(S, 0n), Nat.add(c, Nat.add(d, 0n))), Nat.add(S, Nat.add(0n, Nat.add(c, Nat.add(d, 0n)))), Nat.add(S, Nat.add(c, Nat.add(d, 0n))), NA.add_assoc(S, 0n, Nat.add(c, Nat.add(d, 0n))), Equal.cong(Nat, Nat, z => Nat.add(S, z), Nat.add(0n, Nat.add(c, Nat.add(d, 0n))), Nat.add(c, Nat.add(d, 0n)), Equal.trans(Nat, Nat.add(0n, Nat.add(c, Nat.add(d, 0n))), Nat.add(c, Nat.add(0n, Nat.add(d, 0n))), Nat.add(c, Nat.add(d, 0n)), NA.add_swap(0n, c, Nat.add(d, 0n)), Equal.cong(Nat, Nat, z => Nat.add(c, z), Nat.add(0n, Nat.add(d, 0n)), Nat.add(d, 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(d, 0n)), Nat.add(d, Nat.add(0n, 0n)), Nat.add(d, 0n), NA.add_swap(0n, d, 0n), {==})))))))), Equal.cong(Nat, Nat, z => Nat.add(S, z), Nat.add(c, d), S, hc))
38  L.subst(Nat, z => {Nat.is_le(z, Nat.add(Nat.add(S, d), Nat.div(N, 1n+rp))) == True{} : Bool}, Nat.add(Nat.add(S, d), c), Nat.add(S, S), e2, l4)