proofs/math/typed/f64sqn.bend source

proofs/math/typed/f64sqn.bend on the hub · documented module

import Baseimport ./natlight.bend as NLimport ../../../src/math/natural.bend as Mimport ../../lib/nat.bend as Nimport ../../lib/logic.bend as Limport ../../lib/lemmas/proofs/nat_algebra.bend as NAimport ../natural/arith.bend as NRimport ./width.bend as WWimport ./f64round.bend as FRimport ./f64sqa.bend as AQ# One Newton step for the square root (SoftFloat's f64_sqrt refinement):# from r0 = S + d above S = isqrt(N), with d^2 + 1 <= 12 S, the step# (r0 + floor(N / r0)) / 2 lands in [S, S + 6].def mul1(+y: Nat) -> {Nat.mul(1n, y) == y : Nat}:  NL.mul1(y)def two_mul(+S: Nat) -> {Nat.mul(S, 2n) == Nat.add(S, S) : Nat}:  NL.two_mul(S)def c14(+S: Nat) -> {Nat.mul(S, 14n) == Nat.add(Nat.add(S, S), Nat.mul(S, 12n)) : Nat}:  Equal.trans(Nat, Nat.mul(S, 14n), Nat.mul(14n, S), Nat.add(Nat.add(S, S), Nat.mul(S, 12n)), NA.mul_comm(S, 14n), Equal.trans(Nat, Nat.mul(14n, S), Nat.add(S, Nat.add(S, Nat.mul(12n, S))), Nat.add(Nat.add(S, S), Nat.mul(S, 12n)), {==}, Equal.trans(Nat, Nat.add(S, Nat.add(S, Nat.mul(12n, S))), Nat.add(Nat.add(S, S), Nat.mul(12n, S)), Nat.add(Nat.add(S, S), Nat.mul(S, 12n)), Equal.sym(Nat, Nat.add(Nat.add(S, S), Nat.mul(12n, S)), Nat.add(S, Nat.add(S, Nat.mul(12n, S))), NA.add_assoc(S, S, Nat.mul(12n, S))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(S, S), z), Nat.mul(12n, S), Nat.mul(S, 12n), NA.mul_comm(12n, S)))))def le_cancel_true(+a: Nat, +b: Nat, +c: Nat, +h: {Nat.is_le(a, b) == True{} : Bool}) -> {Nat.is_le(Nat.add(a, c), Nat.add(b, c)) == True{} : Bool}:  Equal.trans(Bool, Nat.is_le(Nat.add(a, c), Nat.add(b, c)), Nat.is_le(a, b), True{}, FR.le_cancel_r(a, b, c), h)# the lower bound: 2 S <= r0 + Q, with S = c + d and r0 = S + ddef 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}:  +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))))))  +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)))  +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)  +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)))  +l3 = L.subst(Nat, z => {Nat.is_le(Nat.mul(c, z), N) == True{} : Bool}, Nat.add(S, d), 1n+rp, hr, l2)  +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)  +l4 = N.le_add_left(c, Nat.div(N, 1n+rp), Nat.add(S, d), hq)  +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))  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)# the product bound: (1 + S)^2 <= c3 * r0 when c3 + d = S + 14 and d^2 + 1 <= 12 Sdef nw_prod(+S: Nat, +d: Nat, +c3: Nat, +hc3: {Nat.add(c3, d) == Nat.add(S, 14n) : Nat}, +hdd: {Nat.is_le(Nat.add(Nat.mul(d, d), 1n), Nat.mul(S, 12n)) == True{} : Bool}) -> {Nat.is_le(Nat.mul(1n+S, 1n+S), Nat.mul(c3, Nat.add(S, d))) == True{} : Bool}:  +ea = Equal.trans(Nat, Nat.mul(Nat.add(c3, d), Nat.add(S, d)), Nat.add(Nat.add(Nat.mul(S, c3), Nat.mul(c3, d)), Nat.add(Nat.mul(S, d), Nat.mul(d, d))), Nat.add(Nat.mul(c3, Nat.add(S, d)), Nat.add(Nat.mul(S, d), Nat.mul(d, d))), Equal.trans(Nat, Nat.mul(Nat.add(c3, d), Nat.add(S, d)), Nat.add(Nat.add(Nat.mul(S, c3), Nat.mul(c3, d)), Nat.add(Nat.mul(S, d), Nat.mul(d, d))), Nat.add(Nat.add(Nat.mul(S, c3), Nat.mul(c3, d)), Nat.add(Nat.mul(S, d), Nat.mul(d, d))), Equal.trans(Nat, Nat.mul(Nat.add(c3, d), Nat.add(S, d)), Nat.add(Nat.add(Nat.mul(S, c3), Nat.mul(c3, d)), Nat.mul(d, Nat.add(S, d))), Nat.add(Nat.add(Nat.mul(S, c3), Nat.mul(c3, d)), Nat.add(Nat.mul(S, d), Nat.mul(d, d))), Equal.trans(Nat, Nat.mul(Nat.add(c3, d), Nat.add(S, d)), Nat.add(Nat.mul(c3, Nat.add(S, d)), Nat.mul(d, Nat.add(S, d))), Nat.add(Nat.add(Nat.mul(S, c3), Nat.mul(c3, d)), Nat.mul(d, Nat.add(S, d))), NA.mul_add_right(c3, d, Nat.add(S, d)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.mul(d, Nat.add(S, d))), Nat.mul(c3, Nat.add(S, d)), Nat.add(Nat.mul(S, c3), Nat.mul(c3, d)), Equal.trans(Nat, Nat.mul(c3, Nat.add(S, d)), Nat.add(Nat.mul(c3, S), Nat.mul(c3, d)), Nat.add(Nat.mul(S, c3), Nat.mul(c3, d)), NA.mul_add_left(c3, S, d), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.mul(c3, d)), Nat.mul(c3, S), Nat.mul(S, c3), NA.mul_comm(c3, S))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.mul(S, c3), Nat.mul(c3, d)), z), Nat.mul(d, Nat.add(S, d)), Nat.add(Nat.mul(S, d), Nat.mul(d, d)), Equal.trans(Nat, Nat.mul(d, Nat.add(S, d)), Nat.add(Nat.mul(d, S), Nat.mul(d, d)), Nat.add(Nat.mul(S, d), Nat.mul(d, d)), NA.mul_add_left(d, S, d), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.mul(d, d)), Nat.mul(d, S), Nat.mul(S, d), NA.mul_comm(d, S))))), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(S, c3), Nat.mul(c3, d)), Nat.add(Nat.mul(S, d), Nat.mul(d, d))), Nat.add(Nat.mul(S, c3), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(c3, d), Nat.add(Nat.mul(d, d), 0n)))), Nat.add(Nat.add(Nat.mul(S, c3), Nat.mul(c3, d)), Nat.add(Nat.mul(S, d), Nat.mul(d, d))), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(S, c3), Nat.mul(c3, d)), Nat.add(Nat.mul(S, d), Nat.mul(d, d))), Nat.add(Nat.add(Nat.mul(S, c3), Nat.add(Nat.mul(c3, d), 0n)), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, d), 0n))), Nat.add(Nat.mul(S, c3), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(c3, d), Nat.add(Nat.mul(d, d), 0n)))), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(S, c3), Nat.mul(c3, d)), Nat.add(Nat.mul(S, d), Nat.mul(d, d))), Nat.add(Nat.add(Nat.mul(S, c3), Nat.add(Nat.mul(c3, d), 0n)), Nat.add(Nat.mul(S, d), Nat.mul(d, d))), Nat.add(Nat.add(Nat.mul(S, c3), Nat.add(Nat.mul(c3, d), 0n)), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, d), 0n))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(Nat.mul(S, d), Nat.mul(d, d))), Nat.add(Nat.mul(S, c3), Nat.mul(c3, d)), Nat.add(Nat.mul(S, c3), Nat.add(Nat.mul(c3, d), 0n)), Equal.trans(Nat, Nat.add(Nat.mul(S, c3), Nat.mul(c3, d)), Nat.add(Nat.add(Nat.mul(S, c3), 0n), Nat.add(Nat.mul(c3, d), 0n)), Nat.add(Nat.mul(S, c3), Nat.add(Nat.mul(c3, d), 0n)), Equal.trans(Nat, Nat.add(Nat.mul(S, c3), Nat.mul(c3, d)), Nat.add(Nat.add(Nat.mul(S, c3), 0n), Nat.mul(c3, d)), Nat.add(Nat.add(Nat.mul(S, c3), 0n), Nat.add(Nat.mul(c3, d), 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.mul(c3, d)), Nat.mul(S, c3), Nat.add(Nat.mul(S, c3), 0n), Equal.sym(Nat, Nat.add(Nat.mul(S, c3), 0n), Nat.mul(S, c3), N.add_zero(Nat.mul(S, c3)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.mul(S, c3), 0n), z), Nat.mul(c3, d), Nat.add(Nat.mul(c3, d), 0n), Equal.sym(Nat, Nat.add(Nat.mul(c3, d), 0n), Nat.mul(c3, d), N.add_zero(Nat.mul(c3, d))))), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(S, c3), 0n), Nat.add(Nat.mul(c3, d), 0n)), Nat.add(Nat.mul(S, c3), Nat.add(0n, Nat.add(Nat.mul(c3, d), 0n))), Nat.add(Nat.mul(S, c3), Nat.add(Nat.mul(c3, d), 0n)), NA.add_assoc(Nat.mul(S, c3), 0n, Nat.add(Nat.mul(c3, d), 0n)), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(S, c3), z), Nat.add(0n, Nat.add(Nat.mul(c3, d), 0n)), Nat.add(Nat.mul(c3, d), 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(Nat.mul(c3, d), 0n)), Nat.add(Nat.mul(c3, d), Nat.add(0n, 0n)), Nat.add(Nat.mul(c3, d), 0n), NA.add_swap(0n, Nat.mul(c3, d), 0n), {==}))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.mul(S, c3), Nat.add(Nat.mul(c3, d), 0n)), z), Nat.add(Nat.mul(S, d), Nat.mul(d, d)), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, d), 0n)), Equal.trans(Nat, Nat.add(Nat.mul(S, d), Nat.mul(d, d)), Nat.add(Nat.add(Nat.mul(S, d), 0n), Nat.add(Nat.mul(d, d), 0n)), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, d), 0n)), Equal.trans(Nat, Nat.add(Nat.mul(S, d), Nat.mul(d, d)), Nat.add(Nat.add(Nat.mul(S, d), 0n), Nat.mul(d, d)), Nat.add(Nat.add(Nat.mul(S, d), 0n), Nat.add(Nat.mul(d, d), 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.mul(d, d)), Nat.mul(S, d), Nat.add(Nat.mul(S, d), 0n), Equal.sym(Nat, Nat.add(Nat.mul(S, d), 0n), Nat.mul(S, d), N.add_zero(Nat.mul(S, d)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.mul(S, 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(S, d), 0n), Nat.add(Nat.mul(d, d), 0n)), Nat.add(Nat.mul(S, d), Nat.add(0n, Nat.add(Nat.mul(d, d), 0n))), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, d), 0n)), NA.add_assoc(Nat.mul(S, d), 0n, Nat.add(Nat.mul(d, d), 0n)), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(S, 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(S, c3), Nat.add(Nat.mul(c3, d), 0n)), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, d), 0n))), Nat.add(Nat.mul(S, c3), Nat.add(Nat.add(Nat.mul(c3, d), 0n), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, d), 0n)))), Nat.add(Nat.mul(S, c3), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(c3, d), Nat.add(Nat.mul(d, d), 0n)))), NA.add_assoc(Nat.mul(S, c3), Nat.add(Nat.mul(c3, d), 0n), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, d), 0n))), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(S, c3), z), Nat.add(Nat.add(Nat.mul(c3, d), 0n), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, d), 0n))), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(c3, d), Nat.add(Nat.mul(d, d), 0n))), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(c3, d), 0n), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, d), 0n))), Nat.add(Nat.mul(c3, d), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, d), 0n))), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(c3, d), Nat.add(Nat.mul(d, d), 0n))), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(c3, d), 0n), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, d), 0n))), Nat.add(Nat.mul(c3, d), Nat.add(0n, Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, d), 0n)))), Nat.add(Nat.mul(c3, d), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, d), 0n))), NA.add_assoc(Nat.mul(c3, d), 0n, Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, d), 0n))), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(c3, d), z), Nat.add(0n, Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, d), 0n))), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, d), 0n)), Equal.trans(Nat, Nat.add(0n, Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, d), 0n))), Nat.add(Nat.mul(S, d), Nat.add(0n, Nat.add(Nat.mul(d, d), 0n))), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, d), 0n)), NA.add_swap(0n, Nat.mul(S, d), Nat.add(Nat.mul(d, d), 0n)), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(S, 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), {==}))))), NA.add_swap(Nat.mul(c3, d), Nat.mul(S, d), Nat.add(Nat.mul(d, d), 0n)))))), Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(S, c3), Nat.mul(c3, d)), Nat.add(Nat.mul(S, d), Nat.mul(d, d))), Nat.add(Nat.mul(S, c3), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(c3, d), Nat.add(Nat.mul(d, d), 0n)))), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(S, c3), Nat.mul(c3, d)), Nat.add(Nat.mul(S, d), Nat.mul(d, d))), Nat.add(Nat.add(Nat.mul(S, c3), Nat.add(Nat.mul(c3, d), 0n)), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, d), 0n))), Nat.add(Nat.mul(S, c3), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(c3, d), Nat.add(Nat.mul(d, d), 0n)))), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(S, c3), Nat.mul(c3, d)), Nat.add(Nat.mul(S, d), Nat.mul(d, d))), Nat.add(Nat.add(Nat.mul(S, c3), Nat.add(Nat.mul(c3, d), 0n)), Nat.add(Nat.mul(S, d), Nat.mul(d, d))), Nat.add(Nat.add(Nat.mul(S, c3), Nat.add(Nat.mul(c3, d), 0n)), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, d), 0n))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(Nat.mul(S, d), Nat.mul(d, d))), Nat.add(Nat.mul(S, c3), Nat.mul(c3, d)), Nat.add(Nat.mul(S, c3), Nat.add(Nat.mul(c3, d), 0n)), Equal.trans(Nat, Nat.add(Nat.mul(S, c3), Nat.mul(c3, d)), Nat.add(Nat.add(Nat.mul(S, c3), 0n), Nat.add(Nat.mul(c3, d), 0n)), Nat.add(Nat.mul(S, c3), Nat.add(Nat.mul(c3, d), 0n)), Equal.trans(Nat, Nat.add(Nat.mul(S, c3), Nat.mul(c3, d)), Nat.add(Nat.add(Nat.mul(S, c3), 0n), Nat.mul(c3, d)), Nat.add(Nat.add(Nat.mul(S, c3), 0n), Nat.add(Nat.mul(c3, d), 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.mul(c3, d)), Nat.mul(S, c3), Nat.add(Nat.mul(S, c3), 0n), Equal.sym(Nat, Nat.add(Nat.mul(S, c3), 0n), Nat.mul(S, c3), N.add_zero(Nat.mul(S, c3)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.mul(S, c3), 0n), z), Nat.mul(c3, d), Nat.add(Nat.mul(c3, d), 0n), Equal.sym(Nat, Nat.add(Nat.mul(c3, d), 0n), Nat.mul(c3, d), N.add_zero(Nat.mul(c3, d))))), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(S, c3), 0n), Nat.add(Nat.mul(c3, d), 0n)), Nat.add(Nat.mul(S, c3), Nat.add(0n, Nat.add(Nat.mul(c3, d), 0n))), Nat.add(Nat.mul(S, c3), Nat.add(Nat.mul(c3, d), 0n)), NA.add_assoc(Nat.mul(S, c3), 0n, Nat.add(Nat.mul(c3, d), 0n)), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(S, c3), z), Nat.add(0n, Nat.add(Nat.mul(c3, d), 0n)), Nat.add(Nat.mul(c3, d), 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(Nat.mul(c3, d), 0n)), Nat.add(Nat.mul(c3, d), Nat.add(0n, 0n)), Nat.add(Nat.mul(c3, d), 0n), NA.add_swap(0n, Nat.mul(c3, d), 0n), {==}))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.mul(S, c3), Nat.add(Nat.mul(c3, d), 0n)), z), Nat.add(Nat.mul(S, d), Nat.mul(d, d)), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, d), 0n)), Equal.trans(Nat, Nat.add(Nat.mul(S, d), Nat.mul(d, d)), Nat.add(Nat.add(Nat.mul(S, d), 0n), Nat.add(Nat.mul(d, d), 0n)), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, d), 0n)), Equal.trans(Nat, Nat.add(Nat.mul(S, d), Nat.mul(d, d)), Nat.add(Nat.add(Nat.mul(S, d), 0n), Nat.mul(d, d)), Nat.add(Nat.add(Nat.mul(S, d), 0n), Nat.add(Nat.mul(d, d), 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.mul(d, d)), Nat.mul(S, d), Nat.add(Nat.mul(S, d), 0n), Equal.sym(Nat, Nat.add(Nat.mul(S, d), 0n), Nat.mul(S, d), N.add_zero(Nat.mul(S, d)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.mul(S, 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(S, d), 0n), Nat.add(Nat.mul(d, d), 0n)), Nat.add(Nat.mul(S, d), Nat.add(0n, Nat.add(Nat.mul(d, d), 0n))), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, d), 0n)), NA.add_assoc(Nat.mul(S, d), 0n, Nat.add(Nat.mul(d, d), 0n)), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(S, 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(S, c3), Nat.add(Nat.mul(c3, d), 0n)), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, d), 0n))), Nat.add(Nat.mul(S, c3), Nat.add(Nat.add(Nat.mul(c3, d), 0n), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, d), 0n)))), Nat.add(Nat.mul(S, c3), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(c3, d), Nat.add(Nat.mul(d, d), 0n)))), NA.add_assoc(Nat.mul(S, c3), Nat.add(Nat.mul(c3, d), 0n), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, d), 0n))), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(S, c3), z), Nat.add(Nat.add(Nat.mul(c3, d), 0n), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, d), 0n))), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(c3, d), Nat.add(Nat.mul(d, d), 0n))), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(c3, d), 0n), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, d), 0n))), Nat.add(Nat.mul(c3, d), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, d), 0n))), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(c3, d), Nat.add(Nat.mul(d, d), 0n))), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(c3, d), 0n), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, d), 0n))), Nat.add(Nat.mul(c3, d), Nat.add(0n, Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, d), 0n)))), Nat.add(Nat.mul(c3, d), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, d), 0n))), NA.add_assoc(Nat.mul(c3, d), 0n, Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, d), 0n))), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(c3, d), z), Nat.add(0n, Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, d), 0n))), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, d), 0n)), Equal.trans(Nat, Nat.add(0n, Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, d), 0n))), Nat.add(Nat.mul(S, d), Nat.add(0n, Nat.add(Nat.mul(d, d), 0n))), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, d), 0n)), NA.add_swap(0n, Nat.mul(S, d), Nat.add(Nat.mul(d, d), 0n)), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(S, 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), {==}))))), NA.add_swap(Nat.mul(c3, d), Nat.mul(S, d), Nat.add(Nat.mul(d, d), 0n))))))))), Equal.sym(Nat, Nat.add(Nat.mul(c3, Nat.add(S, d)), Nat.add(Nat.mul(S, d), Nat.mul(d, d))), Nat.add(Nat.add(Nat.mul(S, c3), Nat.mul(c3, d)), Nat.add(Nat.mul(S, d), Nat.mul(d, d))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(Nat.mul(S, d), Nat.mul(d, d))), Nat.mul(c3, Nat.add(S, d)), Nat.add(Nat.mul(S, c3), Nat.mul(c3, d)), Equal.trans(Nat, Nat.mul(c3, Nat.add(S, d)), Nat.add(Nat.mul(c3, S), Nat.mul(c3, d)), Nat.add(Nat.mul(S, c3), Nat.mul(c3, d)), NA.mul_add_left(c3, S, d), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.mul(c3, d)), Nat.mul(c3, S), Nat.mul(S, c3), NA.mul_comm(c3, S))))))  +eb = Equal.trans(Nat, Nat.mul(Nat.add(S, 14n), Nat.add(S, d)), Nat.add(Nat.add(Nat.mul(S, S), Nat.mul(S, d)), Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n))), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n)))), Equal.trans(Nat, Nat.mul(Nat.add(S, 14n), Nat.add(S, d)), Nat.add(Nat.add(Nat.mul(S, S), Nat.mul(S, d)), Nat.mul(14n, Nat.add(S, d))), Nat.add(Nat.add(Nat.mul(S, S), Nat.mul(S, d)), Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n))), Equal.trans(Nat, Nat.mul(Nat.add(S, 14n), Nat.add(S, d)), Nat.add(Nat.mul(S, Nat.add(S, d)), Nat.mul(14n, Nat.add(S, d))), Nat.add(Nat.add(Nat.mul(S, S), Nat.mul(S, d)), Nat.mul(14n, Nat.add(S, d))), NA.mul_add_right(S, 14n, Nat.add(S, d)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.mul(14n, Nat.add(S, d))), Nat.mul(S, Nat.add(S, d)), Nat.add(Nat.mul(S, S), Nat.mul(S, d)), NA.mul_add_left(S, S, d))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.mul(S, S), Nat.mul(S, d)), z), Nat.mul(14n, Nat.add(S, d)), Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n)), Equal.trans(Nat, Nat.mul(14n, Nat.add(S, d)), Nat.add(Nat.mul(S, 14n), Nat.mul(14n, d)), Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n)), Equal.trans(Nat, Nat.mul(14n, Nat.add(S, d)), Nat.add(Nat.mul(14n, S), Nat.mul(14n, d)), Nat.add(Nat.mul(S, 14n), Nat.mul(14n, d)), NA.mul_add_left(14n, S, d), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.mul(14n, d)), Nat.mul(14n, S), Nat.mul(S, 14n), NA.mul_comm(14n, S))), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(S, 14n), z), Nat.mul(14n, d), Nat.mul(d, 14n), NA.mul_comm(14n, d))))), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(S, S), Nat.mul(S, d)), Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n))), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n)))), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n)))), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(S, S), Nat.mul(S, d)), Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n))), Nat.add(Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, d), 0n)), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n))), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n)))), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(S, S), Nat.mul(S, d)), Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n))), Nat.add(Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, d), 0n)), Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n))), Nat.add(Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, d), 0n)), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n))), Nat.add(Nat.mul(S, S), Nat.mul(S, d)), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, d), 0n)), Equal.trans(Nat, Nat.add(Nat.mul(S, S), Nat.mul(S, d)), Nat.add(Nat.add(Nat.mul(S, S), 0n), Nat.add(Nat.mul(S, d), 0n)), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, d), 0n)), Equal.trans(Nat, Nat.add(Nat.mul(S, S), Nat.mul(S, d)), Nat.add(Nat.add(Nat.mul(S, S), 0n), Nat.mul(S, d)), Nat.add(Nat.add(Nat.mul(S, S), 0n), Nat.add(Nat.mul(S, d), 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.mul(S, d)), Nat.mul(S, S), Nat.add(Nat.mul(S, S), 0n), Equal.sym(Nat, Nat.add(Nat.mul(S, S), 0n), Nat.mul(S, S), N.add_zero(Nat.mul(S, S)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.mul(S, S), 0n), z), Nat.mul(S, d), Nat.add(Nat.mul(S, d), 0n), Equal.sym(Nat, Nat.add(Nat.mul(S, d), 0n), Nat.mul(S, d), N.add_zero(Nat.mul(S, d))))), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(S, S), 0n), Nat.add(Nat.mul(S, d), 0n)), Nat.add(Nat.mul(S, S), Nat.add(0n, Nat.add(Nat.mul(S, d), 0n))), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, d), 0n)), NA.add_assoc(Nat.mul(S, S), 0n, Nat.add(Nat.mul(S, d), 0n)), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(S, S), z), Nat.add(0n, Nat.add(Nat.mul(S, d), 0n)), Nat.add(Nat.mul(S, d), 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(Nat.mul(S, d), 0n)), Nat.add(Nat.mul(S, d), Nat.add(0n, 0n)), Nat.add(Nat.mul(S, d), 0n), NA.add_swap(0n, Nat.mul(S, d), 0n), {==}))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, d), 0n)), z), Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n)), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n)), Equal.trans(Nat, Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n)), Nat.add(Nat.add(Nat.mul(S, 14n), 0n), Nat.add(Nat.mul(d, 14n), 0n)), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n)), Equal.trans(Nat, Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n)), Nat.add(Nat.add(Nat.mul(S, 14n), 0n), Nat.mul(d, 14n)), Nat.add(Nat.add(Nat.mul(S, 14n), 0n), Nat.add(Nat.mul(d, 14n), 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.mul(d, 14n)), Nat.mul(S, 14n), Nat.add(Nat.mul(S, 14n), 0n), Equal.sym(Nat, Nat.add(Nat.mul(S, 14n), 0n), Nat.mul(S, 14n), N.add_zero(Nat.mul(S, 14n)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.mul(S, 14n), 0n), z), Nat.mul(d, 14n), Nat.add(Nat.mul(d, 14n), 0n), Equal.sym(Nat, Nat.add(Nat.mul(d, 14n), 0n), Nat.mul(d, 14n), N.add_zero(Nat.mul(d, 14n))))), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(S, 14n), 0n), Nat.add(Nat.mul(d, 14n), 0n)), Nat.add(Nat.mul(S, 14n), Nat.add(0n, Nat.add(Nat.mul(d, 14n), 0n))), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n)), NA.add_assoc(Nat.mul(S, 14n), 0n, Nat.add(Nat.mul(d, 14n), 0n)), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(S, 14n), z), Nat.add(0n, Nat.add(Nat.mul(d, 14n), 0n)), Nat.add(Nat.mul(d, 14n), 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(Nat.mul(d, 14n), 0n)), Nat.add(Nat.mul(d, 14n), Nat.add(0n, 0n)), Nat.add(Nat.mul(d, 14n), 0n), NA.add_swap(0n, Nat.mul(d, 14n), 0n), {==})))))), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, d), 0n)), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n))), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n)))), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n)))), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, d), 0n)), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n))), Nat.add(Nat.mul(S, S), Nat.add(Nat.add(Nat.mul(S, d), 0n), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n)))), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n)))), NA.add_assoc(Nat.mul(S, S), Nat.add(Nat.mul(S, d), 0n), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n))), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(S, S), z), Nat.add(Nat.add(Nat.mul(S, d), 0n), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n))), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n))), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(S, d), 0n), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n))), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n))), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n))), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(S, d), 0n), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n))), Nat.add(Nat.mul(S, d), Nat.add(0n, Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n)))), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n))), NA.add_assoc(Nat.mul(S, d), 0n, Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n))), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(S, d), z), Nat.add(0n, Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n))), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n)), Equal.trans(Nat, Nat.add(0n, Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n))), Nat.add(Nat.mul(S, 14n), Nat.add(0n, Nat.add(Nat.mul(d, 14n), 0n))), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n)), NA.add_swap(0n, Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n)), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(S, 14n), z), Nat.add(0n, Nat.add(Nat.mul(d, 14n), 0n)), Nat.add(Nat.mul(d, 14n), 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(Nat.mul(d, 14n), 0n)), Nat.add(Nat.mul(d, 14n), Nat.add(0n, 0n)), Nat.add(Nat.mul(d, 14n), 0n), NA.add_swap(0n, Nat.mul(d, 14n), 0n), {==}))))), NA.add_swap(Nat.mul(S, d), Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n))))), NA.add_swap(Nat.mul(S, S), Nat.mul(S, 14n), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n))))), Equal.sym(Nat, Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n)))), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n)))), Equal.trans(Nat, Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n)))), Nat.add(Nat.add(Nat.mul(S, S), 0n), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n)))), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n)))), Equal.trans(Nat, Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n)))), Nat.add(Nat.add(Nat.mul(S, S), 0n), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n)))), Nat.add(Nat.add(Nat.mul(S, S), 0n), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n)))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n)))), Nat.mul(S, S), Nat.add(Nat.mul(S, S), 0n), Equal.sym(Nat, Nat.add(Nat.mul(S, S), 0n), Nat.mul(S, S), N.add_zero(Nat.mul(S, S)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.mul(S, S), 0n), z), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n))), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n))), Equal.trans(Nat, Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n))), Nat.add(Nat.add(Nat.mul(S, d), 0n), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n))), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n))), Equal.trans(Nat, Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n))), Nat.add(Nat.add(Nat.mul(S, d), 0n), Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n))), Nat.add(Nat.add(Nat.mul(S, d), 0n), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n))), Nat.mul(S, d), Nat.add(Nat.mul(S, d), 0n), Equal.sym(Nat, Nat.add(Nat.mul(S, d), 0n), Nat.mul(S, d), N.add_zero(Nat.mul(S, d)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.mul(S, d), 0n), z), Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n)), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n)), Equal.trans(Nat, Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n)), Nat.add(Nat.add(Nat.mul(S, 14n), 0n), Nat.add(Nat.mul(d, 14n), 0n)), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n)), Equal.trans(Nat, Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n)), Nat.add(Nat.add(Nat.mul(S, 14n), 0n), Nat.mul(d, 14n)), Nat.add(Nat.add(Nat.mul(S, 14n), 0n), Nat.add(Nat.mul(d, 14n), 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.mul(d, 14n)), Nat.mul(S, 14n), Nat.add(Nat.mul(S, 14n), 0n), Equal.sym(Nat, Nat.add(Nat.mul(S, 14n), 0n), Nat.mul(S, 14n), N.add_zero(Nat.mul(S, 14n)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.mul(S, 14n), 0n), z), Nat.mul(d, 14n), Nat.add(Nat.mul(d, 14n), 0n), Equal.sym(Nat, Nat.add(Nat.mul(d, 14n), 0n), Nat.mul(d, 14n), N.add_zero(Nat.mul(d, 14n))))), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(S, 14n), 0n), Nat.add(Nat.mul(d, 14n), 0n)), Nat.add(Nat.mul(S, 14n), Nat.add(0n, Nat.add(Nat.mul(d, 14n), 0n))), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n)), NA.add_assoc(Nat.mul(S, 14n), 0n, Nat.add(Nat.mul(d, 14n), 0n)), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(S, 14n), z), Nat.add(0n, Nat.add(Nat.mul(d, 14n), 0n)), Nat.add(Nat.mul(d, 14n), 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(Nat.mul(d, 14n), 0n)), Nat.add(Nat.mul(d, 14n), Nat.add(0n, 0n)), Nat.add(Nat.mul(d, 14n), 0n), NA.add_swap(0n, Nat.mul(d, 14n), 0n), {==})))))), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(S, d), 0n), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n))), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n))), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n))), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(S, d), 0n), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n))), Nat.add(Nat.mul(S, d), Nat.add(0n, Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n)))), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n))), NA.add_assoc(Nat.mul(S, d), 0n, Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n))), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(S, d), z), Nat.add(0n, Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n))), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n)), Equal.trans(Nat, Nat.add(0n, Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n))), Nat.add(Nat.mul(S, 14n), Nat.add(0n, Nat.add(Nat.mul(d, 14n), 0n))), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n)), NA.add_swap(0n, Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n)), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(S, 14n), z), Nat.add(0n, Nat.add(Nat.mul(d, 14n), 0n)), Nat.add(Nat.mul(d, 14n), 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(Nat.mul(d, 14n), 0n)), Nat.add(Nat.mul(d, 14n), Nat.add(0n, 0n)), Nat.add(Nat.mul(d, 14n), 0n), NA.add_swap(0n, Nat.mul(d, 14n), 0n), {==}))))), NA.add_swap(Nat.mul(S, d), Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n)))))), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(S, S), 0n), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n)))), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n)))), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n)))), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(S, S), 0n), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n)))), Nat.add(Nat.mul(S, S), Nat.add(0n, Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n))))), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n)))), NA.add_assoc(Nat.mul(S, S), 0n, Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(S, S), z), Nat.add(0n, Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n)))), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n))), Equal.trans(Nat, Nat.add(0n, Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n)))), Nat.add(Nat.mul(S, 14n), Nat.add(0n, Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n)))), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n))), NA.add_swap(0n, Nat.mul(S, 14n), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n))), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(S, 14n), z), Nat.add(0n, Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n))), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n)), Equal.trans(Nat, Nat.add(0n, Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n))), Nat.add(Nat.mul(S, d), Nat.add(0n, Nat.add(Nat.mul(d, 14n), 0n))), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n)), NA.add_swap(0n, Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n)), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(S, d), z), Nat.add(0n, Nat.add(Nat.mul(d, 14n), 0n)), Nat.add(Nat.mul(d, 14n), 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(Nat.mul(d, 14n), 0n)), Nat.add(Nat.mul(d, 14n), Nat.add(0n, 0n)), Nat.add(Nat.mul(d, 14n), 0n), NA.add_swap(0n, Nat.mul(d, 14n), 0n), {==}))))))), NA.add_swap(Nat.mul(S, S), Nat.mul(S, 14n), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n))))))))  +ec = Equal.trans(Nat, Nat.add(Nat.mul(c3, Nat.add(S, d)), Nat.add(Nat.mul(S, d), Nat.mul(d, d))), Nat.mul(Nat.add(c3, d), Nat.add(S, d)), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n)))), Equal.sym(Nat, Nat.mul(Nat.add(c3, d), Nat.add(S, d)), Nat.add(Nat.mul(c3, Nat.add(S, d)), Nat.add(Nat.mul(S, d), Nat.mul(d, d))), ea), Equal.trans(Nat, Nat.mul(Nat.add(c3, d), Nat.add(S, d)), Nat.mul(Nat.add(S, 14n), Nat.add(S, d)), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n)))), Equal.cong(Nat, Nat, z => Nat.mul(z, Nat.add(S, d)), Nat.add(c3, d), Nat.add(S, 14n), hc3), eb))  +ed = NR.add_cancel(Nat.mul(S, d), Nat.add(Nat.mul(c3, Nat.add(S, d)), Nat.mul(d, d)), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n))), Equal.trans(Nat, Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(c3, Nat.add(S, d)), Nat.mul(d, d))), Nat.add(Nat.mul(c3, Nat.add(S, d)), Nat.add(Nat.mul(S, d), Nat.mul(d, d))), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n)))), Equal.trans(Nat, Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(c3, Nat.add(S, d)), Nat.mul(d, d))), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(c3, Nat.add(S, d)), Nat.add(Nat.mul(d, d), 0n))), Nat.add(Nat.mul(c3, Nat.add(S, d)), Nat.add(Nat.mul(S, d), Nat.mul(d, d))), Equal.trans(Nat, Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(c3, Nat.add(S, d)), Nat.mul(d, d))), Nat.add(Nat.add(Nat.mul(S, d), 0n), Nat.add(Nat.mul(c3, Nat.add(S, d)), Nat.add(Nat.mul(d, d), 0n))), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(c3, Nat.add(S, d)), Nat.add(Nat.mul(d, d), 0n))), Equal.trans(Nat, Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(c3, Nat.add(S, d)), Nat.mul(d, d))), Nat.add(Nat.add(Nat.mul(S, d), 0n), Nat.add(Nat.mul(c3, Nat.add(S, d)), Nat.mul(d, d))), Nat.add(Nat.add(Nat.mul(S, d), 0n), Nat.add(Nat.mul(c3, Nat.add(S, d)), Nat.add(Nat.mul(d, d), 0n))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(Nat.mul(c3, Nat.add(S, d)), Nat.mul(d, d))), Nat.mul(S, d), Nat.add(Nat.mul(S, d), 0n), Equal.sym(Nat, Nat.add(Nat.mul(S, d), 0n), Nat.mul(S, d), N.add_zero(Nat.mul(S, d)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.mul(S, d), 0n), z), Nat.add(Nat.mul(c3, Nat.add(S, d)), Nat.mul(d, d)), Nat.add(Nat.mul(c3, Nat.add(S, d)), Nat.add(Nat.mul(d, d), 0n)), Equal.trans(Nat, Nat.add(Nat.mul(c3, Nat.add(S, d)), Nat.mul(d, d)), Nat.add(Nat.add(Nat.mul(c3, Nat.add(S, d)), 0n), Nat.add(Nat.mul(d, d), 0n)), Nat.add(Nat.mul(c3, Nat.add(S, d)), Nat.add(Nat.mul(d, d), 0n)), Equal.trans(Nat, Nat.add(Nat.mul(c3, Nat.add(S, d)), Nat.mul(d, d)), Nat.add(Nat.add(Nat.mul(c3, Nat.add(S, d)), 0n), Nat.mul(d, d)), Nat.add(Nat.add(Nat.mul(c3, Nat.add(S, d)), 0n), Nat.add(Nat.mul(d, d), 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.mul(d, d)), Nat.mul(c3, Nat.add(S, d)), Nat.add(Nat.mul(c3, Nat.add(S, d)), 0n), Equal.sym(Nat, Nat.add(Nat.mul(c3, Nat.add(S, d)), 0n), Nat.mul(c3, Nat.add(S, d)), N.add_zero(Nat.mul(c3, Nat.add(S, d))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.mul(c3, Nat.add(S, 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(c3, Nat.add(S, d)), 0n), Nat.add(Nat.mul(d, d), 0n)), Nat.add(Nat.mul(c3, Nat.add(S, d)), Nat.add(0n, Nat.add(Nat.mul(d, d), 0n))), Nat.add(Nat.mul(c3, Nat.add(S, d)), Nat.add(Nat.mul(d, d), 0n)), NA.add_assoc(Nat.mul(c3, Nat.add(S, d)), 0n, Nat.add(Nat.mul(d, d), 0n)), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(c3, Nat.add(S, 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(S, d), 0n), Nat.add(Nat.mul(c3, Nat.add(S, d)), Nat.add(Nat.mul(d, d), 0n))), Nat.add(Nat.mul(S, d), Nat.add(0n, Nat.add(Nat.mul(c3, Nat.add(S, d)), Nat.add(Nat.mul(d, d), 0n)))), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(c3, Nat.add(S, d)), Nat.add(Nat.mul(d, d), 0n))), NA.add_assoc(Nat.mul(S, d), 0n, Nat.add(Nat.mul(c3, Nat.add(S, d)), Nat.add(Nat.mul(d, d), 0n))), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(S, d), z), Nat.add(0n, Nat.add(Nat.mul(c3, Nat.add(S, d)), Nat.add(Nat.mul(d, d), 0n))), Nat.add(Nat.mul(c3, Nat.add(S, d)), Nat.add(Nat.mul(d, d), 0n)), Equal.trans(Nat, Nat.add(0n, Nat.add(Nat.mul(c3, Nat.add(S, d)), Nat.add(Nat.mul(d, d), 0n))), Nat.add(Nat.mul(c3, Nat.add(S, d)), Nat.add(0n, Nat.add(Nat.mul(d, d), 0n))), Nat.add(Nat.mul(c3, Nat.add(S, d)), Nat.add(Nat.mul(d, d), 0n)), NA.add_swap(0n, Nat.mul(c3, Nat.add(S, d)), Nat.add(Nat.mul(d, d), 0n)), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(c3, Nat.add(S, 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(c3, Nat.add(S, d)), Nat.add(Nat.mul(S, d), Nat.mul(d, d))), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(c3, Nat.add(S, d)), Nat.add(Nat.mul(d, d), 0n))), Equal.trans(Nat, Nat.add(Nat.mul(c3, Nat.add(S, d)), Nat.add(Nat.mul(S, d), Nat.mul(d, d))), Nat.add(Nat.add(Nat.mul(c3, Nat.add(S, d)), 0n), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, d), 0n))), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(c3, Nat.add(S, d)), Nat.add(Nat.mul(d, d), 0n))), Equal.trans(Nat, Nat.add(Nat.mul(c3, Nat.add(S, d)), Nat.add(Nat.mul(S, d), Nat.mul(d, d))), Nat.add(Nat.add(Nat.mul(c3, Nat.add(S, d)), 0n), Nat.add(Nat.mul(S, d), Nat.mul(d, d))), Nat.add(Nat.add(Nat.mul(c3, Nat.add(S, d)), 0n), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, d), 0n))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(Nat.mul(S, d), Nat.mul(d, d))), Nat.mul(c3, Nat.add(S, d)), Nat.add(Nat.mul(c3, Nat.add(S, d)), 0n), Equal.sym(Nat, Nat.add(Nat.mul(c3, Nat.add(S, d)), 0n), Nat.mul(c3, Nat.add(S, d)), N.add_zero(Nat.mul(c3, Nat.add(S, d))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.mul(c3, Nat.add(S, d)), 0n), z), Nat.add(Nat.mul(S, d), Nat.mul(d, d)), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, d), 0n)), Equal.trans(Nat, Nat.add(Nat.mul(S, d), Nat.mul(d, d)), Nat.add(Nat.add(Nat.mul(S, d), 0n), Nat.add(Nat.mul(d, d), 0n)), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, d), 0n)), Equal.trans(Nat, Nat.add(Nat.mul(S, d), Nat.mul(d, d)), Nat.add(Nat.add(Nat.mul(S, d), 0n), Nat.mul(d, d)), Nat.add(Nat.add(Nat.mul(S, d), 0n), Nat.add(Nat.mul(d, d), 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.mul(d, d)), Nat.mul(S, d), Nat.add(Nat.mul(S, d), 0n), Equal.sym(Nat, Nat.add(Nat.mul(S, d), 0n), Nat.mul(S, d), N.add_zero(Nat.mul(S, d)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.mul(S, 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(S, d), 0n), Nat.add(Nat.mul(d, d), 0n)), Nat.add(Nat.mul(S, d), Nat.add(0n, Nat.add(Nat.mul(d, d), 0n))), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, d), 0n)), NA.add_assoc(Nat.mul(S, d), 0n, Nat.add(Nat.mul(d, d), 0n)), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(S, 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(c3, Nat.add(S, d)), 0n), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, d), 0n))), Nat.add(Nat.mul(c3, Nat.add(S, d)), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, d), 0n))), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(c3, Nat.add(S, d)), Nat.add(Nat.mul(d, d), 0n))), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(c3, Nat.add(S, d)), 0n), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, d), 0n))), Nat.add(Nat.mul(c3, Nat.add(S, d)), Nat.add(0n, Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, d), 0n)))), Nat.add(Nat.mul(c3, Nat.add(S, d)), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, d), 0n))), NA.add_assoc(Nat.mul(c3, Nat.add(S, d)), 0n, Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, d), 0n))), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(c3, Nat.add(S, d)), z), Nat.add(0n, Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, d), 0n))), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, d), 0n)), Equal.trans(Nat, Nat.add(0n, Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, d), 0n))), Nat.add(Nat.mul(S, d), Nat.add(0n, Nat.add(Nat.mul(d, d), 0n))), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, d), 0n)), NA.add_swap(0n, Nat.mul(S, d), Nat.add(Nat.mul(d, d), 0n)), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(S, 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), {==}))))), NA.add_swap(Nat.mul(c3, Nat.add(S, d)), Nat.mul(S, d), Nat.add(Nat.mul(d, d), 0n)))))), Equal.trans(Nat, Nat.add(Nat.mul(c3, Nat.add(S, d)), Nat.add(Nat.mul(S, d), Nat.mul(d, d))), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n)))), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n)))), ec, Equal.trans(Nat, Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n)))), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n)))), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n)))), Equal.trans(Nat, Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n)))), Nat.add(Nat.add(Nat.mul(S, S), 0n), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n)))), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n)))), Equal.trans(Nat, Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n)))), Nat.add(Nat.add(Nat.mul(S, S), 0n), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n)))), Nat.add(Nat.add(Nat.mul(S, S), 0n), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n)))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n)))), Nat.mul(S, S), Nat.add(Nat.mul(S, S), 0n), Equal.sym(Nat, Nat.add(Nat.mul(S, S), 0n), Nat.mul(S, S), N.add_zero(Nat.mul(S, S)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.mul(S, S), 0n), z), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n))), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n))), Equal.trans(Nat, Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n))), Nat.add(Nat.add(Nat.mul(S, d), 0n), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n))), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n))), Equal.trans(Nat, Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n))), Nat.add(Nat.add(Nat.mul(S, d), 0n), Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n))), Nat.add(Nat.add(Nat.mul(S, d), 0n), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n))), Nat.mul(S, d), Nat.add(Nat.mul(S, d), 0n), Equal.sym(Nat, Nat.add(Nat.mul(S, d), 0n), Nat.mul(S, d), N.add_zero(Nat.mul(S, d)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.mul(S, d), 0n), z), Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n)), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n)), Equal.trans(Nat, Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n)), Nat.add(Nat.add(Nat.mul(S, 14n), 0n), Nat.add(Nat.mul(d, 14n), 0n)), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n)), Equal.trans(Nat, Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n)), Nat.add(Nat.add(Nat.mul(S, 14n), 0n), Nat.mul(d, 14n)), Nat.add(Nat.add(Nat.mul(S, 14n), 0n), Nat.add(Nat.mul(d, 14n), 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.mul(d, 14n)), Nat.mul(S, 14n), Nat.add(Nat.mul(S, 14n), 0n), Equal.sym(Nat, Nat.add(Nat.mul(S, 14n), 0n), Nat.mul(S, 14n), N.add_zero(Nat.mul(S, 14n)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.mul(S, 14n), 0n), z), Nat.mul(d, 14n), Nat.add(Nat.mul(d, 14n), 0n), Equal.sym(Nat, Nat.add(Nat.mul(d, 14n), 0n), Nat.mul(d, 14n), N.add_zero(Nat.mul(d, 14n))))), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(S, 14n), 0n), Nat.add(Nat.mul(d, 14n), 0n)), Nat.add(Nat.mul(S, 14n), Nat.add(0n, Nat.add(Nat.mul(d, 14n), 0n))), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n)), NA.add_assoc(Nat.mul(S, 14n), 0n, Nat.add(Nat.mul(d, 14n), 0n)), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(S, 14n), z), Nat.add(0n, Nat.add(Nat.mul(d, 14n), 0n)), Nat.add(Nat.mul(d, 14n), 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(Nat.mul(d, 14n), 0n)), Nat.add(Nat.mul(d, 14n), Nat.add(0n, 0n)), Nat.add(Nat.mul(d, 14n), 0n), NA.add_swap(0n, Nat.mul(d, 14n), 0n), {==})))))), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(S, d), 0n), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n))), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n))), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n))), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(S, d), 0n), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n))), Nat.add(Nat.mul(S, d), Nat.add(0n, Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n)))), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n))), NA.add_assoc(Nat.mul(S, d), 0n, Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n))), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(S, d), z), Nat.add(0n, Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n))), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n)), Equal.trans(Nat, Nat.add(0n, Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n))), Nat.add(Nat.mul(S, 14n), Nat.add(0n, Nat.add(Nat.mul(d, 14n), 0n))), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n)), NA.add_swap(0n, Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n)), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(S, 14n), z), Nat.add(0n, Nat.add(Nat.mul(d, 14n), 0n)), Nat.add(Nat.mul(d, 14n), 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(Nat.mul(d, 14n), 0n)), Nat.add(Nat.mul(d, 14n), Nat.add(0n, 0n)), Nat.add(Nat.mul(d, 14n), 0n), NA.add_swap(0n, Nat.mul(d, 14n), 0n), {==}))))), NA.add_swap(Nat.mul(S, d), Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n)))))), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(S, S), 0n), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n)))), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n)))), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n)))), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(S, S), 0n), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n)))), Nat.add(Nat.mul(S, S), Nat.add(0n, Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n))))), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n)))), NA.add_assoc(Nat.mul(S, S), 0n, Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(S, S), z), Nat.add(0n, Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n)))), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n))), Equal.trans(Nat, Nat.add(0n, Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n)))), Nat.add(Nat.mul(S, 14n), Nat.add(0n, Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n)))), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n))), NA.add_swap(0n, Nat.mul(S, 14n), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n))), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(S, 14n), z), Nat.add(0n, Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n))), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n)), Equal.trans(Nat, Nat.add(0n, Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n))), Nat.add(Nat.mul(S, d), Nat.add(0n, Nat.add(Nat.mul(d, 14n), 0n))), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n)), NA.add_swap(0n, Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n)), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(S, d), z), Nat.add(0n, Nat.add(Nat.mul(d, 14n), 0n)), Nat.add(Nat.mul(d, 14n), 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(Nat.mul(d, 14n), 0n)), Nat.add(Nat.mul(d, 14n), Nat.add(0n, 0n)), Nat.add(Nat.mul(d, 14n), 0n), NA.add_swap(0n, Nat.mul(d, 14n), 0n), {==}))))))), NA.add_swap(Nat.mul(S, S), Nat.mul(S, 14n), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n))))), Equal.sym(Nat, Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n)))), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n)))), Equal.trans(Nat, Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n)))), Nat.add(Nat.add(Nat.mul(S, d), 0n), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(d, 14n), 0n)))), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n)))), Equal.trans(Nat, Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n)))), Nat.add(Nat.add(Nat.mul(S, d), 0n), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n)))), Nat.add(Nat.add(Nat.mul(S, d), 0n), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(d, 14n), 0n)))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n)))), Nat.mul(S, d), Nat.add(Nat.mul(S, d), 0n), Equal.sym(Nat, Nat.add(Nat.mul(S, d), 0n), Nat.mul(S, d), N.add_zero(Nat.mul(S, d)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.mul(S, d), 0n), z), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n))), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(d, 14n), 0n))), Equal.trans(Nat, Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n))), Nat.add(Nat.add(Nat.mul(S, S), 0n), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n))), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(d, 14n), 0n))), Equal.trans(Nat, Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n))), Nat.add(Nat.add(Nat.mul(S, S), 0n), Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n))), Nat.add(Nat.add(Nat.mul(S, S), 0n), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n))), Nat.mul(S, S), Nat.add(Nat.mul(S, S), 0n), Equal.sym(Nat, Nat.add(Nat.mul(S, S), 0n), Nat.mul(S, S), N.add_zero(Nat.mul(S, S)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.mul(S, S), 0n), z), Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n)), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n)), Equal.trans(Nat, Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n)), Nat.add(Nat.add(Nat.mul(S, 14n), 0n), Nat.add(Nat.mul(d, 14n), 0n)), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n)), Equal.trans(Nat, Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n)), Nat.add(Nat.add(Nat.mul(S, 14n), 0n), Nat.mul(d, 14n)), Nat.add(Nat.add(Nat.mul(S, 14n), 0n), Nat.add(Nat.mul(d, 14n), 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.mul(d, 14n)), Nat.mul(S, 14n), Nat.add(Nat.mul(S, 14n), 0n), Equal.sym(Nat, Nat.add(Nat.mul(S, 14n), 0n), Nat.mul(S, 14n), N.add_zero(Nat.mul(S, 14n)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.mul(S, 14n), 0n), z), Nat.mul(d, 14n), Nat.add(Nat.mul(d, 14n), 0n), Equal.sym(Nat, Nat.add(Nat.mul(d, 14n), 0n), Nat.mul(d, 14n), N.add_zero(Nat.mul(d, 14n))))), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(S, 14n), 0n), Nat.add(Nat.mul(d, 14n), 0n)), Nat.add(Nat.mul(S, 14n), Nat.add(0n, Nat.add(Nat.mul(d, 14n), 0n))), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n)), NA.add_assoc(Nat.mul(S, 14n), 0n, Nat.add(Nat.mul(d, 14n), 0n)), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(S, 14n), z), Nat.add(0n, Nat.add(Nat.mul(d, 14n), 0n)), Nat.add(Nat.mul(d, 14n), 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(Nat.mul(d, 14n), 0n)), Nat.add(Nat.mul(d, 14n), Nat.add(0n, 0n)), Nat.add(Nat.mul(d, 14n), 0n), NA.add_swap(0n, Nat.mul(d, 14n), 0n), {==})))))), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(S, S), 0n), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n))), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n))), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(d, 14n), 0n))), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(S, S), 0n), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n))), Nat.add(Nat.mul(S, S), Nat.add(0n, Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n)))), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n))), NA.add_assoc(Nat.mul(S, S), 0n, Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n))), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(S, S), z), Nat.add(0n, Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n))), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n)), Equal.trans(Nat, Nat.add(0n, Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n))), Nat.add(Nat.mul(S, 14n), Nat.add(0n, Nat.add(Nat.mul(d, 14n), 0n))), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n)), NA.add_swap(0n, Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n)), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(S, 14n), z), Nat.add(0n, Nat.add(Nat.mul(d, 14n), 0n)), Nat.add(Nat.mul(d, 14n), 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(Nat.mul(d, 14n), 0n)), Nat.add(Nat.mul(d, 14n), Nat.add(0n, 0n)), Nat.add(Nat.mul(d, 14n), 0n), NA.add_swap(0n, Nat.mul(d, 14n), 0n), {==}))))), NA.add_swap(Nat.mul(S, S), Nat.mul(S, 14n), Nat.add(Nat.mul(d, 14n), 0n)))))), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(S, d), 0n), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(d, 14n), 0n)))), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(d, 14n), 0n)))), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n)))), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(S, d), 0n), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(d, 14n), 0n)))), Nat.add(Nat.mul(S, d), Nat.add(0n, Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(d, 14n), 0n))))), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(d, 14n), 0n)))), NA.add_assoc(Nat.mul(S, d), 0n, Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(d, 14n), 0n)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(S, d), z), Nat.add(0n, Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(d, 14n), 0n)))), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(d, 14n), 0n))), Equal.trans(Nat, Nat.add(0n, Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(d, 14n), 0n)))), Nat.add(Nat.mul(S, 14n), Nat.add(0n, Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(d, 14n), 0n)))), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(d, 14n), 0n))), NA.add_swap(0n, Nat.mul(S, 14n), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(d, 14n), 0n))), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(S, 14n), z), Nat.add(0n, Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(d, 14n), 0n))), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(d, 14n), 0n)), Equal.trans(Nat, Nat.add(0n, Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(d, 14n), 0n))), Nat.add(Nat.mul(S, S), Nat.add(0n, Nat.add(Nat.mul(d, 14n), 0n))), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(d, 14n), 0n)), NA.add_swap(0n, Nat.mul(S, S), Nat.add(Nat.mul(d, 14n), 0n)), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(S, S), z), Nat.add(0n, Nat.add(Nat.mul(d, 14n), 0n)), Nat.add(Nat.mul(d, 14n), 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(Nat.mul(d, 14n), 0n)), Nat.add(Nat.mul(d, 14n), Nat.add(0n, 0n)), Nat.add(Nat.mul(d, 14n), 0n), NA.add_swap(0n, Nat.mul(d, 14n), 0n), {==}))))))), Equal.trans(Nat, Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(d, 14n), 0n)))), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(d, 14n), 0n)))), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n)))), NA.add_swap(Nat.mul(S, d), Nat.mul(S, 14n), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(d, 14n), 0n))), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(S, 14n), z), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(d, 14n), 0n))), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, d), Nat.add(Nat.mul(d, 14n), 0n))), NA.add_swap(Nat.mul(S, d), Nat.mul(S, S), Nat.add(Nat.mul(d, 14n), 0n)))))))))))  +ex = Equal.cong(Nat, Nat, z => Nat.add(1n+S, z), Nat.mul(S, 1n+S), Nat.add(S, Nat.mul(S, S)), NA.mul_succ(S, S))  +e1 = Equal.trans(Nat, Nat.add(Nat.mul(1n+S, 1n+S), Nat.mul(d, d)), Nat.add(Nat.add(1n+S, Nat.add(S, Nat.mul(S, S))), Nat.mul(d, d)), Nat.add(Nat.add(Nat.add(Nat.mul(d, d), 1n), Nat.add(S, S)), Nat.mul(S, S)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.mul(d, d)), Nat.mul(1n+S, 1n+S), Nat.add(1n+S, Nat.add(S, Nat.mul(S, S))), ex), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(1n, S), Nat.add(S, Nat.mul(S, S))), Nat.mul(d, d)), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(d, d), Nat.add(S, Nat.add(S, 1n)))), Nat.add(Nat.add(Nat.add(Nat.mul(d, d), 1n), Nat.add(S, S)), Nat.mul(S, S)), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(1n, S), Nat.add(S, Nat.mul(S, S))), Nat.mul(d, d)), Nat.add(Nat.add(Nat.mul(S, S), Nat.add(S, Nat.add(S, 1n))), Nat.add(Nat.mul(d, d), 0n)), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(d, d), Nat.add(S, Nat.add(S, 1n)))), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(1n, S), Nat.add(S, Nat.mul(S, S))), Nat.mul(d, d)), Nat.add(Nat.add(Nat.mul(S, S), Nat.add(S, Nat.add(S, 1n))), Nat.mul(d, d)), Nat.add(Nat.add(Nat.mul(S, S), Nat.add(S, Nat.add(S, 1n))), Nat.add(Nat.mul(d, d), 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.mul(d, d)), Nat.add(Nat.add(1n, S), Nat.add(S, Nat.mul(S, S))), Nat.add(Nat.mul(S, S), Nat.add(S, Nat.add(S, 1n))), Equal.trans(Nat, Nat.add(Nat.add(1n, S), Nat.add(S, Nat.mul(S, S))), Nat.add(Nat.add(S, 1n), Nat.add(Nat.mul(S, S), Nat.add(S, 0n))), Nat.add(Nat.mul(S, S), Nat.add(S, Nat.add(S, 1n))), Equal.trans(Nat, Nat.add(Nat.add(1n, S), Nat.add(S, Nat.mul(S, S))), Nat.add(Nat.add(S, 1n), Nat.add(S, Nat.mul(S, S))), Nat.add(Nat.add(S, 1n), Nat.add(Nat.mul(S, S), Nat.add(S, 0n))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(S, Nat.mul(S, S))), Nat.add(1n, S), Nat.add(S, 1n), Equal.trans(Nat, Nat.add(1n, S), Nat.add(1n, Nat.add(S, 0n)), Nat.add(S, 1n), Equal.cong(Nat, Nat, z => Nat.add(1n, z), S, Nat.add(S, 0n), Equal.sym(Nat, Nat.add(S, 0n), S, N.add_zero(S))), Equal.trans(Nat, Nat.add(1n, Nat.add(S, 0n)), Nat.add(S, Nat.add(1n, 0n)), Nat.add(S, 1n), NA.add_swap(1n, S, 0n), {==}))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(S, 1n), z), Nat.add(S, Nat.mul(S, S)), Nat.add(Nat.mul(S, S), Nat.add(S, 0n)), Equal.trans(Nat, Nat.add(S, Nat.mul(S, S)), Nat.add(Nat.add(S, 0n), Nat.add(Nat.mul(S, S), 0n)), Nat.add(Nat.mul(S, S), Nat.add(S, 0n)), Equal.trans(Nat, Nat.add(S, Nat.mul(S, S)), Nat.add(Nat.add(S, 0n), Nat.mul(S, S)), Nat.add(Nat.add(S, 0n), Nat.add(Nat.mul(S, S), 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.mul(S, S)), 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.mul(S, S), Nat.add(Nat.mul(S, S), 0n), Equal.sym(Nat, Nat.add(Nat.mul(S, S), 0n), Nat.mul(S, S), N.add_zero(Nat.mul(S, S))))), Equal.trans(Nat, Nat.add(Nat.add(S, 0n), Nat.add(Nat.mul(S, S), 0n)), Nat.add(S, Nat.add(Nat.mul(S, S), 0n)), Nat.add(Nat.mul(S, S), Nat.add(S, 0n)), Equal.trans(Nat, Nat.add(Nat.add(S, 0n), Nat.add(Nat.mul(S, S), 0n)), Nat.add(S, Nat.add(0n, Nat.add(Nat.mul(S, S), 0n))), Nat.add(S, Nat.add(Nat.mul(S, S), 0n)), NA.add_assoc(S, 0n, Nat.add(Nat.mul(S, S), 0n)), Equal.cong(Nat, Nat, z => Nat.add(S, z), Nat.add(0n, Nat.add(Nat.mul(S, S), 0n)), Nat.add(Nat.mul(S, S), 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(Nat.mul(S, S), 0n)), Nat.add(Nat.mul(S, S), Nat.add(0n, 0n)), Nat.add(Nat.mul(S, S), 0n), NA.add_swap(0n, Nat.mul(S, S), 0n), {==}))), NA.add_swap(S, Nat.mul(S, S), 0n))))), Equal.trans(Nat, Nat.add(Nat.add(S, 1n), Nat.add(Nat.mul(S, S), Nat.add(S, 0n))), Nat.add(S, Nat.add(Nat.mul(S, S), Nat.add(S, 1n))), Nat.add(Nat.mul(S, S), Nat.add(S, Nat.add(S, 1n))), Equal.trans(Nat, Nat.add(Nat.add(S, 1n), Nat.add(Nat.mul(S, S), Nat.add(S, 0n))), Nat.add(S, Nat.add(1n, Nat.add(Nat.mul(S, S), Nat.add(S, 0n)))), Nat.add(S, Nat.add(Nat.mul(S, S), Nat.add(S, 1n))), NA.add_assoc(S, 1n, Nat.add(Nat.mul(S, S), Nat.add(S, 0n))), Equal.cong(Nat, Nat, z => Nat.add(S, z), Nat.add(1n, Nat.add(Nat.mul(S, S), Nat.add(S, 0n))), Nat.add(Nat.mul(S, S), Nat.add(S, 1n)), Equal.trans(Nat, Nat.add(1n, Nat.add(Nat.mul(S, S), Nat.add(S, 0n))), Nat.add(Nat.mul(S, S), Nat.add(1n, Nat.add(S, 0n))), Nat.add(Nat.mul(S, S), Nat.add(S, 1n)), NA.add_swap(1n, Nat.mul(S, S), Nat.add(S, 0n)), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(S, S), z), Nat.add(1n, Nat.add(S, 0n)), Nat.add(S, 1n), Equal.trans(Nat, Nat.add(1n, Nat.add(S, 0n)), Nat.add(S, Nat.add(1n, 0n)), Nat.add(S, 1n), NA.add_swap(1n, S, 0n), {==}))))), NA.add_swap(S, Nat.mul(S, S), Nat.add(S, 1n))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.mul(S, S), Nat.add(S, Nat.add(S, 1n))), 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(S, S), Nat.add(S, Nat.add(S, 1n))), Nat.add(Nat.mul(d, d), 0n)), Nat.add(Nat.mul(S, S), Nat.add(Nat.add(S, Nat.add(S, 1n)), Nat.add(Nat.mul(d, d), 0n))), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(d, d), Nat.add(S, Nat.add(S, 1n)))), NA.add_assoc(Nat.mul(S, S), Nat.add(S, Nat.add(S, 1n)), Nat.add(Nat.mul(d, d), 0n)), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(S, S), z), Nat.add(Nat.add(S, Nat.add(S, 1n)), Nat.add(Nat.mul(d, d), 0n)), Nat.add(Nat.mul(d, d), Nat.add(S, Nat.add(S, 1n))), Equal.trans(Nat, Nat.add(Nat.add(S, Nat.add(S, 1n)), Nat.add(Nat.mul(d, d), 0n)), Nat.add(S, Nat.add(Nat.mul(d, d), Nat.add(S, 1n))), Nat.add(Nat.mul(d, d), Nat.add(S, Nat.add(S, 1n))), Equal.trans(Nat, Nat.add(Nat.add(S, Nat.add(S, 1n)), Nat.add(Nat.mul(d, d), 0n)), Nat.add(S, Nat.add(Nat.add(S, 1n), Nat.add(Nat.mul(d, d), 0n))), Nat.add(S, Nat.add(Nat.mul(d, d), Nat.add(S, 1n))), NA.add_assoc(S, Nat.add(S, 1n), Nat.add(Nat.mul(d, d), 0n)), Equal.cong(Nat, Nat, z => Nat.add(S, z), Nat.add(Nat.add(S, 1n), Nat.add(Nat.mul(d, d), 0n)), Nat.add(Nat.mul(d, d), Nat.add(S, 1n)), Equal.trans(Nat, Nat.add(Nat.add(S, 1n), Nat.add(Nat.mul(d, d), 0n)), Nat.add(S, Nat.add(Nat.mul(d, d), 1n)), Nat.add(Nat.mul(d, d), Nat.add(S, 1n)), Equal.trans(Nat, Nat.add(Nat.add(S, 1n), Nat.add(Nat.mul(d, d), 0n)), Nat.add(S, Nat.add(1n, Nat.add(Nat.mul(d, d), 0n))), Nat.add(S, Nat.add(Nat.mul(d, d), 1n)), NA.add_assoc(S, 1n, Nat.add(Nat.mul(d, d), 0n)), Equal.cong(Nat, Nat, z => Nat.add(S, z), Nat.add(1n, Nat.add(Nat.mul(d, d), 0n)), Nat.add(Nat.mul(d, d), 1n), Equal.trans(Nat, Nat.add(1n, Nat.add(Nat.mul(d, d), 0n)), Nat.add(Nat.mul(d, d), Nat.add(1n, 0n)), Nat.add(Nat.mul(d, d), 1n), NA.add_swap(1n, Nat.mul(d, d), 0n), {==}))), NA.add_swap(S, Nat.mul(d, d), 1n)))), NA.add_swap(S, Nat.mul(d, d), Nat.add(S, 1n)))))), Equal.sym(Nat, Nat.add(Nat.add(Nat.add(Nat.mul(d, d), 1n), Nat.add(S, S)), Nat.mul(S, S)), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(d, d), Nat.add(S, Nat.add(S, 1n)))), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.mul(d, d), 1n), Nat.add(S, S)), Nat.mul(S, S)), Nat.add(Nat.add(Nat.mul(d, d), Nat.add(S, Nat.add(S, 1n))), Nat.add(Nat.mul(S, S), 0n)), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(d, d), Nat.add(S, Nat.add(S, 1n)))), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.mul(d, d), 1n), Nat.add(S, S)), Nat.mul(S, S)), Nat.add(Nat.add(Nat.mul(d, d), Nat.add(S, Nat.add(S, 1n))), Nat.mul(S, S)), Nat.add(Nat.add(Nat.mul(d, d), Nat.add(S, Nat.add(S, 1n))), Nat.add(Nat.mul(S, S), 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.mul(S, S)), Nat.add(Nat.add(Nat.mul(d, d), 1n), Nat.add(S, S)), Nat.add(Nat.mul(d, d), Nat.add(S, Nat.add(S, 1n))), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(d, d), 1n), Nat.add(S, S)), Nat.add(Nat.add(Nat.mul(d, d), 1n), Nat.add(S, Nat.add(S, 0n))), Nat.add(Nat.mul(d, d), Nat.add(S, Nat.add(S, 1n))), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(d, d), 1n), Nat.add(S, S)), Nat.add(Nat.add(Nat.mul(d, d), 1n), Nat.add(S, S)), Nat.add(Nat.add(Nat.mul(d, d), 1n), Nat.add(S, Nat.add(S, 0n))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(S, S)), Nat.add(Nat.mul(d, d), 1n), Nat.add(Nat.mul(d, d), 1n), Equal.trans(Nat, Nat.add(Nat.mul(d, d), 1n), Nat.add(Nat.add(Nat.mul(d, d), 0n), 1n), Nat.add(Nat.mul(d, d), 1n), Equal.cong(Nat, Nat, z => Nat.add(z, 1n), 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(d, d), 0n), 1n), Nat.add(Nat.mul(d, d), Nat.add(0n, 1n)), Nat.add(Nat.mul(d, d), 1n), NA.add_assoc(Nat.mul(d, d), 0n, 1n), {==}))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.mul(d, d), 1n), z), Nat.add(S, S), Nat.add(S, Nat.add(S, 0n)), Equal.trans(Nat, Nat.add(S, S), Nat.add(Nat.add(S, 0n), Nat.add(S, 0n)), Nat.add(S, Nat.add(S, 0n)), Equal.trans(Nat, Nat.add(S, S), Nat.add(Nat.add(S, 0n), S), Nat.add(Nat.add(S, 0n), Nat.add(S, 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, S), 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), S, Nat.add(S, 0n), Equal.sym(Nat, Nat.add(S, 0n), S, N.add_zero(S)))), Equal.trans(Nat, Nat.add(Nat.add(S, 0n), Nat.add(S, 0n)), Nat.add(S, Nat.add(0n, Nat.add(S, 0n))), Nat.add(S, Nat.add(S, 0n)), NA.add_assoc(S, 0n, Nat.add(S, 0n)), Equal.cong(Nat, Nat, z => Nat.add(S, z), Nat.add(0n, Nat.add(S, 0n)), Nat.add(S, 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(S, 0n)), Nat.add(S, Nat.add(0n, 0n)), Nat.add(S, 0n), NA.add_swap(0n, S, 0n), {==})))))), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(d, d), 1n), Nat.add(S, Nat.add(S, 0n))), Nat.add(Nat.mul(d, d), Nat.add(1n, Nat.add(S, Nat.add(S, 0n)))), Nat.add(Nat.mul(d, d), Nat.add(S, Nat.add(S, 1n))), NA.add_assoc(Nat.mul(d, d), 1n, Nat.add(S, Nat.add(S, 0n))), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(d, d), z), Nat.add(1n, Nat.add(S, Nat.add(S, 0n))), Nat.add(S, Nat.add(S, 1n)), Equal.trans(Nat, Nat.add(1n, Nat.add(S, Nat.add(S, 0n))), Nat.add(S, Nat.add(1n, Nat.add(S, 0n))), Nat.add(S, Nat.add(S, 1n)), NA.add_swap(1n, S, Nat.add(S, 0n)), Equal.cong(Nat, Nat, z => Nat.add(S, z), Nat.add(1n, Nat.add(S, 0n)), Nat.add(S, 1n), Equal.trans(Nat, Nat.add(1n, Nat.add(S, 0n)), Nat.add(S, Nat.add(1n, 0n)), Nat.add(S, 1n), NA.add_swap(1n, S, 0n), {==}))))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.mul(d, d), Nat.add(S, Nat.add(S, 1n))), z), Nat.mul(S, S), Nat.add(Nat.mul(S, S), 0n), Equal.sym(Nat, Nat.add(Nat.mul(S, S), 0n), Nat.mul(S, S), N.add_zero(Nat.mul(S, S))))), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(d, d), Nat.add(S, Nat.add(S, 1n))), Nat.add(Nat.mul(S, S), 0n)), Nat.add(Nat.mul(d, d), Nat.add(Nat.mul(S, S), Nat.add(S, Nat.add(S, 1n)))), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(d, d), Nat.add(S, Nat.add(S, 1n)))), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(d, d), Nat.add(S, Nat.add(S, 1n))), Nat.add(Nat.mul(S, S), 0n)), Nat.add(Nat.mul(d, d), Nat.add(Nat.add(S, Nat.add(S, 1n)), Nat.add(Nat.mul(S, S), 0n))), Nat.add(Nat.mul(d, d), Nat.add(Nat.mul(S, S), Nat.add(S, Nat.add(S, 1n)))), NA.add_assoc(Nat.mul(d, d), Nat.add(S, Nat.add(S, 1n)), Nat.add(Nat.mul(S, S), 0n)), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(d, d), z), Nat.add(Nat.add(S, Nat.add(S, 1n)), Nat.add(Nat.mul(S, S), 0n)), Nat.add(Nat.mul(S, S), Nat.add(S, Nat.add(S, 1n))), Equal.trans(Nat, Nat.add(Nat.add(S, Nat.add(S, 1n)), Nat.add(Nat.mul(S, S), 0n)), Nat.add(S, Nat.add(Nat.mul(S, S), Nat.add(S, 1n))), Nat.add(Nat.mul(S, S), Nat.add(S, Nat.add(S, 1n))), Equal.trans(Nat, Nat.add(Nat.add(S, Nat.add(S, 1n)), Nat.add(Nat.mul(S, S), 0n)), Nat.add(S, Nat.add(Nat.add(S, 1n), Nat.add(Nat.mul(S, S), 0n))), Nat.add(S, Nat.add(Nat.mul(S, S), Nat.add(S, 1n))), NA.add_assoc(S, Nat.add(S, 1n), Nat.add(Nat.mul(S, S), 0n)), Equal.cong(Nat, Nat, z => Nat.add(S, z), Nat.add(Nat.add(S, 1n), Nat.add(Nat.mul(S, S), 0n)), Nat.add(Nat.mul(S, S), Nat.add(S, 1n)), Equal.trans(Nat, Nat.add(Nat.add(S, 1n), Nat.add(Nat.mul(S, S), 0n)), Nat.add(S, Nat.add(Nat.mul(S, S), 1n)), Nat.add(Nat.mul(S, S), Nat.add(S, 1n)), Equal.trans(Nat, Nat.add(Nat.add(S, 1n), Nat.add(Nat.mul(S, S), 0n)), Nat.add(S, Nat.add(1n, Nat.add(Nat.mul(S, S), 0n))), Nat.add(S, Nat.add(Nat.mul(S, S), 1n)), NA.add_assoc(S, 1n, Nat.add(Nat.mul(S, S), 0n)), Equal.cong(Nat, Nat, z => Nat.add(S, z), Nat.add(1n, Nat.add(Nat.mul(S, S), 0n)), Nat.add(Nat.mul(S, S), 1n), Equal.trans(Nat, Nat.add(1n, Nat.add(Nat.mul(S, S), 0n)), Nat.add(Nat.mul(S, S), Nat.add(1n, 0n)), Nat.add(Nat.mul(S, S), 1n), NA.add_swap(1n, Nat.mul(S, S), 0n), {==}))), NA.add_swap(S, Nat.mul(S, S), 1n)))), NA.add_swap(S, Nat.mul(S, S), Nat.add(S, 1n))))), NA.add_swap(Nat.mul(d, d), Nat.mul(S, S), Nat.add(S, Nat.add(S, 1n))))))))  +l1 = Equal.trans(Bool, Nat.is_le(Nat.add(Nat.add(Nat.add(Nat.mul(d, d), 1n), Nat.add(S, S)), Nat.mul(S, S)), Nat.add(Nat.add(Nat.mul(S, 12n), Nat.add(S, S)), Nat.mul(S, S))), Nat.is_le(Nat.add(Nat.add(Nat.mul(d, d), 1n), Nat.add(Nat.add(S, S), Nat.mul(S, S))), Nat.add(Nat.mul(S, 12n), Nat.add(Nat.add(S, S), Nat.mul(S, S)))), True{}, Equal.trans(Bool, Nat.is_le(Nat.add(Nat.add(Nat.add(Nat.mul(d, d), 1n), Nat.add(S, S)), Nat.mul(S, S)), Nat.add(Nat.add(Nat.mul(S, 12n), Nat.add(S, S)), Nat.mul(S, S))), Nat.is_le(Nat.add(Nat.add(Nat.mul(d, d), 1n), Nat.add(Nat.add(S, S), Nat.mul(S, S))), Nat.add(Nat.mul(S, 12n), Nat.add(Nat.add(S, S), Nat.mul(S, S)))), Nat.is_le(Nat.add(Nat.add(Nat.mul(d, d), 1n), Nat.add(Nat.add(S, S), Nat.mul(S, S))), Nat.add(Nat.mul(S, 12n), Nat.add(Nat.add(S, S), Nat.mul(S, S)))), Equal.trans(Bool, Nat.is_le(Nat.add(Nat.add(Nat.add(Nat.mul(d, d), 1n), Nat.add(S, S)), Nat.mul(S, S)), Nat.add(Nat.add(Nat.mul(S, 12n), Nat.add(S, S)), Nat.mul(S, S))), Nat.is_le(Nat.add(Nat.add(Nat.mul(d, d), 1n), Nat.add(Nat.add(S, S), Nat.mul(S, S))), Nat.add(Nat.add(Nat.mul(S, 12n), Nat.add(S, S)), Nat.mul(S, S))), Nat.is_le(Nat.add(Nat.add(Nat.mul(d, d), 1n), Nat.add(Nat.add(S, S), Nat.mul(S, S))), Nat.add(Nat.mul(S, 12n), Nat.add(Nat.add(S, S), Nat.mul(S, S)))), Equal.cong(Nat, Bool, z => Nat.is_le(z, Nat.add(Nat.add(Nat.mul(S, 12n), Nat.add(S, S)), Nat.mul(S, S))), Nat.add(Nat.add(Nat.add(Nat.mul(d, d), 1n), Nat.add(S, S)), Nat.mul(S, S)), Nat.add(Nat.add(Nat.mul(d, d), 1n), Nat.add(Nat.add(S, S), Nat.mul(S, S))), NA.add_assoc(Nat.add(Nat.mul(d, d), 1n), Nat.add(S, S), Nat.mul(S, S))), Equal.cong(Nat, Bool, z => Nat.is_le(Nat.add(Nat.add(Nat.mul(d, d), 1n), Nat.add(Nat.add(S, S), Nat.mul(S, S))), z), Nat.add(Nat.add(Nat.mul(S, 12n), Nat.add(S, S)), Nat.mul(S, S)), Nat.add(Nat.mul(S, 12n), Nat.add(Nat.add(S, S), Nat.mul(S, S))), NA.add_assoc(Nat.mul(S, 12n), Nat.add(S, S), Nat.mul(S, S)))), {==}), le_cancel_true(Nat.add(Nat.mul(d, d), 1n), Nat.mul(S, 12n), Nat.add(Nat.add(S, S), Nat.mul(S, S)), hdd))  +e2 = Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(S, 12n), Nat.add(S, S)), Nat.mul(S, S)), Nat.add(Nat.mul(S, 14n), Nat.mul(S, S)), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, 14n), 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.mul(S, S)), Nat.add(Nat.mul(S, 12n), Nat.add(S, S)), Nat.mul(S, 14n), Equal.trans(Nat, Nat.add(Nat.mul(S, 12n), Nat.add(S, S)), Nat.add(Nat.add(S, S), Nat.mul(S, 12n)), Nat.mul(S, 14n), NA.add_comm(Nat.mul(S, 12n), Nat.add(S, S)), Equal.sym(Nat, Nat.mul(S, 14n), Nat.add(Nat.add(S, S), Nat.mul(S, 12n)), c14(S)))), Equal.trans(Nat, Nat.add(Nat.mul(S, 14n), Nat.mul(S, S)), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, S), 0n)), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, 14n), 0n)), Equal.trans(Nat, Nat.add(Nat.mul(S, 14n), Nat.mul(S, S)), Nat.add(Nat.add(Nat.mul(S, 14n), 0n), Nat.add(Nat.mul(S, S), 0n)), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, S), 0n)), Equal.trans(Nat, Nat.add(Nat.mul(S, 14n), Nat.mul(S, S)), Nat.add(Nat.add(Nat.mul(S, 14n), 0n), Nat.mul(S, S)), Nat.add(Nat.add(Nat.mul(S, 14n), 0n), Nat.add(Nat.mul(S, S), 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.mul(S, S)), Nat.mul(S, 14n), Nat.add(Nat.mul(S, 14n), 0n), Equal.sym(Nat, Nat.add(Nat.mul(S, 14n), 0n), Nat.mul(S, 14n), N.add_zero(Nat.mul(S, 14n)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.mul(S, 14n), 0n), z), Nat.mul(S, S), Nat.add(Nat.mul(S, S), 0n), Equal.sym(Nat, Nat.add(Nat.mul(S, S), 0n), Nat.mul(S, S), N.add_zero(Nat.mul(S, S))))), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(S, 14n), 0n), Nat.add(Nat.mul(S, S), 0n)), Nat.add(Nat.mul(S, 14n), Nat.add(0n, Nat.add(Nat.mul(S, S), 0n))), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, S), 0n)), NA.add_assoc(Nat.mul(S, 14n), 0n, Nat.add(Nat.mul(S, S), 0n)), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(S, 14n), z), Nat.add(0n, Nat.add(Nat.mul(S, S), 0n)), Nat.add(Nat.mul(S, S), 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(Nat.mul(S, S), 0n)), Nat.add(Nat.mul(S, S), Nat.add(0n, 0n)), Nat.add(Nat.mul(S, S), 0n), NA.add_swap(0n, Nat.mul(S, S), 0n), {==})))), Equal.sym(Nat, Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, 14n), 0n)), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, S), 0n)), Equal.trans(Nat, Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, 14n), 0n)), Nat.add(Nat.add(Nat.mul(S, S), 0n), Nat.add(Nat.mul(S, 14n), 0n)), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, S), 0n)), Equal.trans(Nat, Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, 14n), 0n)), Nat.add(Nat.add(Nat.mul(S, S), 0n), Nat.add(Nat.mul(S, 14n), 0n)), Nat.add(Nat.add(Nat.mul(S, S), 0n), Nat.add(Nat.mul(S, 14n), 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(Nat.mul(S, 14n), 0n)), Nat.mul(S, S), Nat.add(Nat.mul(S, S), 0n), Equal.sym(Nat, Nat.add(Nat.mul(S, S), 0n), Nat.mul(S, S), N.add_zero(Nat.mul(S, S)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.mul(S, S), 0n), z), Nat.add(Nat.mul(S, 14n), 0n), Nat.add(Nat.mul(S, 14n), 0n), Equal.trans(Nat, Nat.add(Nat.mul(S, 14n), 0n), Nat.add(Nat.add(Nat.mul(S, 14n), 0n), 0n), Nat.add(Nat.mul(S, 14n), 0n), Equal.cong(Nat, Nat, z => Nat.add(z, 0n), Nat.mul(S, 14n), Nat.add(Nat.mul(S, 14n), 0n), Equal.sym(Nat, Nat.add(Nat.mul(S, 14n), 0n), Nat.mul(S, 14n), N.add_zero(Nat.mul(S, 14n)))), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(S, 14n), 0n), 0n), Nat.add(Nat.mul(S, 14n), Nat.add(0n, 0n)), Nat.add(Nat.mul(S, 14n), 0n), NA.add_assoc(Nat.mul(S, 14n), 0n, 0n), {==})))), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(S, S), 0n), Nat.add(Nat.mul(S, 14n), 0n)), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, 14n), 0n)), Nat.add(Nat.mul(S, 14n), Nat.add(Nat.mul(S, S), 0n)), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(S, S), 0n), Nat.add(Nat.mul(S, 14n), 0n)), Nat.add(Nat.mul(S, S), Nat.add(0n, Nat.add(Nat.mul(S, 14n), 0n))), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, 14n), 0n)), NA.add_assoc(Nat.mul(S, S), 0n, Nat.add(Nat.mul(S, 14n), 0n)), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(S, S), z), Nat.add(0n, Nat.add(Nat.mul(S, 14n), 0n)), Nat.add(Nat.mul(S, 14n), 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(Nat.mul(S, 14n), 0n)), Nat.add(Nat.mul(S, 14n), Nat.add(0n, 0n)), Nat.add(Nat.mul(S, 14n), 0n), NA.add_swap(0n, Nat.mul(S, 14n), 0n), {==}))), NA.add_swap(Nat.mul(S, S), Nat.mul(S, 14n), 0n))))))  +l2 = L.subst(Nat, z => {Nat.is_le(Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, 14n), 0n)), z) == True{} : Bool}, Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n))), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n))), {==}, N.le_add_left(Nat.add(Nat.mul(S, 14n), 0n), Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n)), Nat.mul(S, S), N.le_add_left(0n, Nat.mul(d, 14n), Nat.mul(S, 14n), N.zero_le(Nat.mul(d, 14n)))))  +l3 = N.le_trans(Nat.add(Nat.mul(1n+S, 1n+S), Nat.mul(d, d)), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, 14n), 0n)), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n))), L.subst(Nat, z => {Nat.is_le(Nat.add(Nat.mul(1n+S, 1n+S), Nat.mul(d, d)), z) == True{} : Bool}, Nat.add(Nat.add(Nat.mul(S, 12n), Nat.add(S, S)), Nat.mul(S, S)), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, 14n), 0n)), e2, L.subst(Nat, z => {Nat.is_le(z, Nat.add(Nat.add(Nat.mul(S, 12n), Nat.add(S, S)), Nat.mul(S, S))) == True{} : Bool}, Nat.add(Nat.add(Nat.add(Nat.mul(d, d), 1n), Nat.add(S, S)), Nat.mul(S, S)), Nat.add(Nat.mul(1n+S, 1n+S), Nat.mul(d, d)), Equal.sym(Nat, Nat.add(Nat.mul(1n+S, 1n+S), Nat.mul(d, d)), Nat.add(Nat.add(Nat.add(Nat.mul(d, d), 1n), Nat.add(S, S)), Nat.mul(S, S)), e1), l1)), l2)  +l4 = L.subst(Nat, z => {Nat.is_le(Nat.add(Nat.mul(1n+S, 1n+S), Nat.mul(d, d)), z) == True{} : Bool}, Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n))), Nat.add(Nat.mul(c3, Nat.add(S, d)), Nat.mul(d, d)), Equal.sym(Nat, Nat.add(Nat.mul(c3, Nat.add(S, d)), Nat.mul(d, d)), Nat.add(Nat.mul(S, S), Nat.add(Nat.mul(S, 14n), Nat.mul(d, 14n))), ed), l3)  Equal.trans(Bool, Nat.is_le(Nat.mul(1n+S, 1n+S), Nat.mul(c3, Nat.add(S, d))), Nat.is_le(Nat.add(Nat.mul(1n+S, 1n+S), Nat.mul(d, d)), Nat.add(Nat.mul(c3, Nat.add(S, d)), Nat.mul(d, d))), True{}, Equal.sym(Bool, Nat.is_le(Nat.add(Nat.mul(1n+S, 1n+S), Nat.mul(d, d)), Nat.add(Nat.mul(c3, Nat.add(S, d)), Nat.mul(d, d))), Nat.is_le(Nat.mul(1n+S, 1n+S), Nat.mul(c3, Nat.add(S, d))), FR.le_cancel_r(Nat.mul(1n+S, 1n+S), Nat.mul(c3, Nat.add(S, d)), Nat.mul(d, d))), l4)# the upper bound: r0 + Q <= 2 S + 13def nw_hi(+N: Nat, +S: Nat, +d: Nat, +rp: Nat, +c3: Nat, +hS: {S == M.isqrt(N) : Nat}, +hr: {Nat.add(S, d) == 1n+rp : Nat}, +hc3: {Nat.add(c3, d) == Nat.add(S, 14n) : Nat}, +hdd: {Nat.is_le(Nat.add(Nat.mul(d, d), 1n), Nat.mul(S, 12n)) == True{} : Bool}) -> {Nat.is_le(Nat.add(Nat.add(S, d), Nat.div(N, 1n+rp)), Nat.add(13n, Nat.add(S, S))) == True{} : Bool}:  +hN = L.subst(Nat, z => {Nat.is_lt(N, Nat.mul(1n+z, 1n+z)) == True{} : Bool}, M.isqrt(N), S, Equal.sym(Nat, S, M.isqrt(N), hS), AQ.ilt(N))  +h1 = N.lt_le_trans(N, Nat.mul(1n+S, 1n+S), Nat.mul(c3, 1n+rp), hN, L.subst(Nat, z => {Nat.is_le(Nat.mul(1n+S, 1n+S), Nat.mul(c3, z)) == True{} : Bool}, Nat.add(S, d), 1n+rp, hr, nw_prod(S, d, c3, hc3, hdd)))  +h2 = Equal.trans(Bool, Nat.is_le(c3, Nat.div(N, 1n+rp)), Nat.is_le(Nat.mul(c3, 1n+rp), N), False{}, NR.le_div(rp, c3, N), N.lt_not_le(N, Nat.mul(c3, 1n+rp), h1))  +h3 = N.not_le_lt(c3, Nat.div(N, 1n+rp), h2)  +h4 = Equal.trans(Bool, Nat.is_lt(Nat.add(Nat.add(S, d), Nat.div(N, 1n+rp)), Nat.add(Nat.add(S, d), c3)), Nat.is_lt(Nat.div(N, 1n+rp), c3), True{}, WW.lt_cancel_l(Nat.add(S, d), Nat.div(N, 1n+rp), c3), h3)  +e1 = Equal.trans(Nat, Nat.add(Nat.add(S, d), c3), Nat.add(S, Nat.add(c3, d)), Nat.add(14n, Nat.add(S, S)), Equal.trans(Nat, Nat.add(Nat.add(S, d), c3), Nat.add(S, Nat.add(c3, Nat.add(d, 0n))), Nat.add(S, Nat.add(c3, d)), Equal.trans(Nat, Nat.add(Nat.add(S, d), c3), Nat.add(Nat.add(S, Nat.add(d, 0n)), Nat.add(c3, 0n)), Nat.add(S, Nat.add(c3, Nat.add(d, 0n))), Equal.trans(Nat, Nat.add(Nat.add(S, d), c3), Nat.add(Nat.add(S, Nat.add(d, 0n)), c3), Nat.add(Nat.add(S, Nat.add(d, 0n)), Nat.add(c3, 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, c3), 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), c3, Nat.add(c3, 0n), Equal.sym(Nat, Nat.add(c3, 0n), c3, N.add_zero(c3)))), Equal.trans(Nat, Nat.add(Nat.add(S, Nat.add(d, 0n)), Nat.add(c3, 0n)), Nat.add(S, Nat.add(Nat.add(d, 0n), Nat.add(c3, 0n))), Nat.add(S, Nat.add(c3, Nat.add(d, 0n))), NA.add_assoc(S, Nat.add(d, 0n), Nat.add(c3, 0n)), Equal.cong(Nat, Nat, z => Nat.add(S, z), Nat.add(Nat.add(d, 0n), Nat.add(c3, 0n)), Nat.add(c3, Nat.add(d, 0n)), Equal.trans(Nat, Nat.add(Nat.add(d, 0n), Nat.add(c3, 0n)), Nat.add(d, Nat.add(c3, 0n)), Nat.add(c3, Nat.add(d, 0n)), Equal.trans(Nat, Nat.add(Nat.add(d, 0n), Nat.add(c3, 0n)), Nat.add(d, Nat.add(0n, Nat.add(c3, 0n))), Nat.add(d, Nat.add(c3, 0n)), NA.add_assoc(d, 0n, Nat.add(c3, 0n)), Equal.cong(Nat, Nat, z => Nat.add(d, z), Nat.add(0n, Nat.add(c3, 0n)), Nat.add(c3, 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(c3, 0n)), Nat.add(c3, Nat.add(0n, 0n)), Nat.add(c3, 0n), NA.add_swap(0n, c3, 0n), {==}))), NA.add_swap(d, c3, 0n))))), Equal.sym(Nat, Nat.add(S, Nat.add(c3, d)), Nat.add(S, Nat.add(c3, Nat.add(d, 0n))), Equal.trans(Nat, Nat.add(S, Nat.add(c3, d)), Nat.add(Nat.add(S, 0n), Nat.add(c3, Nat.add(d, 0n))), Nat.add(S, Nat.add(c3, Nat.add(d, 0n))), Equal.trans(Nat, Nat.add(S, Nat.add(c3, d)), Nat.add(Nat.add(S, 0n), Nat.add(c3, d)), Nat.add(Nat.add(S, 0n), Nat.add(c3, Nat.add(d, 0n))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(c3, 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(c3, d), Nat.add(c3, Nat.add(d, 0n)), Equal.trans(Nat, Nat.add(c3, d), Nat.add(Nat.add(c3, 0n), Nat.add(d, 0n)), Nat.add(c3, Nat.add(d, 0n)), Equal.trans(Nat, Nat.add(c3, d), Nat.add(Nat.add(c3, 0n), d), Nat.add(Nat.add(c3, 0n), Nat.add(d, 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, d), c3, Nat.add(c3, 0n), Equal.sym(Nat, Nat.add(c3, 0n), c3, N.add_zero(c3))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(c3, 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(c3, 0n), Nat.add(d, 0n)), Nat.add(c3, Nat.add(0n, Nat.add(d, 0n))), Nat.add(c3, Nat.add(d, 0n)), NA.add_assoc(c3, 0n, Nat.add(d, 0n)), Equal.cong(Nat, Nat, z => Nat.add(c3, 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(c3, Nat.add(d, 0n))), Nat.add(S, Nat.add(0n, Nat.add(c3, Nat.add(d, 0n)))), Nat.add(S, Nat.add(c3, Nat.add(d, 0n))), NA.add_assoc(S, 0n, Nat.add(c3, Nat.add(d, 0n))), Equal.cong(Nat, Nat, z => Nat.add(S, z), Nat.add(0n, Nat.add(c3, Nat.add(d, 0n))), Nat.add(c3, Nat.add(d, 0n)), Equal.trans(Nat, Nat.add(0n, Nat.add(c3, Nat.add(d, 0n))), Nat.add(c3, Nat.add(0n, Nat.add(d, 0n))), Nat.add(c3, Nat.add(d, 0n)), NA.add_swap(0n, c3, Nat.add(d, 0n)), Equal.cong(Nat, Nat, z => Nat.add(c3, 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(S, Nat.add(c3, d)), Nat.add(S, Nat.add(S, 14n)), Nat.add(14n, Nat.add(S, S)), Equal.cong(Nat, Nat, z => Nat.add(S, z), Nat.add(c3, d), Nat.add(S, 14n), hc3), Equal.trans(Nat, Nat.add(S, Nat.add(S, 14n)), Nat.add(S, Nat.add(S, 14n)), Nat.add(14n, Nat.add(S, S)), Equal.trans(Nat, Nat.add(S, Nat.add(S, 14n)), Nat.add(Nat.add(S, 0n), Nat.add(S, 14n)), Nat.add(S, Nat.add(S, 14n)), Equal.trans(Nat, Nat.add(S, Nat.add(S, 14n)), Nat.add(Nat.add(S, 0n), Nat.add(S, 14n)), Nat.add(Nat.add(S, 0n), Nat.add(S, 14n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(S, 14n)), 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(S, 14n), Nat.add(S, 14n), Equal.trans(Nat, Nat.add(S, 14n), Nat.add(Nat.add(S, 0n), 14n), Nat.add(S, 14n), Equal.cong(Nat, Nat, z => Nat.add(z, 14n), S, Nat.add(S, 0n), Equal.sym(Nat, Nat.add(S, 0n), S, N.add_zero(S))), Equal.trans(Nat, Nat.add(Nat.add(S, 0n), 14n), Nat.add(S, Nat.add(0n, 14n)), Nat.add(S, 14n), NA.add_assoc(S, 0n, 14n), {==})))), Equal.trans(Nat, Nat.add(Nat.add(S, 0n), Nat.add(S, 14n)), Nat.add(S, Nat.add(0n, Nat.add(S, 14n))), Nat.add(S, Nat.add(S, 14n)), NA.add_assoc(S, 0n, Nat.add(S, 14n)), Equal.cong(Nat, Nat, z => Nat.add(S, z), Nat.add(0n, Nat.add(S, 14n)), Nat.add(S, 14n), Equal.trans(Nat, Nat.add(0n, Nat.add(S, 14n)), Nat.add(S, Nat.add(0n, 14n)), Nat.add(S, 14n), NA.add_swap(0n, S, 14n), {==})))), Equal.sym(Nat, Nat.add(14n, Nat.add(S, S)), Nat.add(S, Nat.add(S, 14n)), Equal.trans(Nat, Nat.add(14n, Nat.add(S, S)), Nat.add(14n, Nat.add(S, Nat.add(S, 0n))), Nat.add(S, Nat.add(S, 14n)), Equal.cong(Nat, Nat, z => Nat.add(14n, z), Nat.add(S, S), Nat.add(S, Nat.add(S, 0n)), Equal.trans(Nat, Nat.add(S, S), Nat.add(Nat.add(S, 0n), Nat.add(S, 0n)), Nat.add(S, Nat.add(S, 0n)), Equal.trans(Nat, Nat.add(S, S), Nat.add(Nat.add(S, 0n), S), Nat.add(Nat.add(S, 0n), Nat.add(S, 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, S), 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), S, Nat.add(S, 0n), Equal.sym(Nat, Nat.add(S, 0n), S, N.add_zero(S)))), Equal.trans(Nat, Nat.add(Nat.add(S, 0n), Nat.add(S, 0n)), Nat.add(S, Nat.add(0n, Nat.add(S, 0n))), Nat.add(S, Nat.add(S, 0n)), NA.add_assoc(S, 0n, Nat.add(S, 0n)), Equal.cong(Nat, Nat, z => Nat.add(S, z), Nat.add(0n, Nat.add(S, 0n)), Nat.add(S, 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(S, 0n)), Nat.add(S, Nat.add(0n, 0n)), Nat.add(S, 0n), NA.add_swap(0n, S, 0n), {==}))))), Equal.trans(Nat, Nat.add(14n, Nat.add(S, Nat.add(S, 0n))), Nat.add(S, Nat.add(14n, Nat.add(S, 0n))), Nat.add(S, Nat.add(S, 14n)), NA.add_swap(14n, S, Nat.add(S, 0n)), Equal.cong(Nat, Nat, z => Nat.add(S, z), Nat.add(14n, Nat.add(S, 0n)), Nat.add(S, 14n), Equal.trans(Nat, Nat.add(14n, Nat.add(S, 0n)), Nat.add(S, Nat.add(14n, 0n)), Nat.add(S, 14n), NA.add_swap(14n, S, 0n), {==}))))))))  N.lt_succ_le(Nat.add(Nat.add(S, d), Nat.div(N, 1n+rp)), Nat.add(13n, Nat.add(S, S)), L.subst(Nat, z => {Nat.is_lt(Nat.add(Nat.add(S, d), Nat.div(N, 1n+rp)), z) == True{} : Bool}, Nat.add(Nat.add(S, d), c3), Nat.add(14n, Nat.add(S, S)), e1, h4))# halving: S <= (r0 + Q) / 2 <= S + 6def half_lo(+S: Nat, +n: Nat, +h: {Nat.is_le(Nat.add(S, S), n) == True{} : Bool}) -> {Nat.is_le(S, Nat.div(n, 2n)) == True{} : Bool}:  Equal.trans(Bool, Nat.is_le(S, Nat.div(n, 2n)), Nat.is_le(Nat.mul(S, 2n), n), True{}, NR.le_div(1n, S, n), L.subst(Nat, z => {Nat.is_le(z, n) == True{} : Bool}, Nat.add(S, S), Nat.mul(S, 2n), Equal.sym(Nat, Nat.mul(S, 2n), Nat.add(S, S), two_mul(S)), h))def half_hi(+S: Nat, +n: Nat, +h: {Nat.is_le(n, Nat.add(13n, Nat.add(S, S))) == True{} : Bool}) -> {Nat.is_le(Nat.div(n, 2n), Nat.add(6n, S)) == True{} : Bool}:  +e = Equal.trans(Nat, Nat.mul(Nat.add(7n, S), 2n), Nat.add(Nat.add(7n, S), Nat.add(7n, S)), Nat.add(14n, Nat.add(S, S)), two_mul(Nat.add(7n, S)), Equal.trans(Nat, Nat.add(Nat.add(7n, S), Nat.add(7n, S)), Nat.add(S, Nat.add(S, 14n)), Nat.add(14n, Nat.add(S, S)), Equal.trans(Nat, Nat.add(Nat.add(7n, S), Nat.add(7n, S)), Nat.add(Nat.add(S, 7n), Nat.add(S, 7n)), Nat.add(S, Nat.add(S, 14n)), Equal.trans(Nat, Nat.add(Nat.add(7n, S), Nat.add(7n, S)), Nat.add(Nat.add(S, 7n), Nat.add(7n, S)), Nat.add(Nat.add(S, 7n), Nat.add(S, 7n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(7n, S)), Nat.add(7n, S), Nat.add(S, 7n), Equal.trans(Nat, Nat.add(7n, S), Nat.add(7n, Nat.add(S, 0n)), Nat.add(S, 7n), Equal.cong(Nat, Nat, z => Nat.add(7n, z), S, Nat.add(S, 0n), Equal.sym(Nat, Nat.add(S, 0n), S, N.add_zero(S))), Equal.trans(Nat, Nat.add(7n, Nat.add(S, 0n)), Nat.add(S, Nat.add(7n, 0n)), Nat.add(S, 7n), NA.add_swap(7n, S, 0n), {==}))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(S, 7n), z), Nat.add(7n, S), Nat.add(S, 7n), Equal.trans(Nat, Nat.add(7n, S), Nat.add(7n, Nat.add(S, 0n)), Nat.add(S, 7n), Equal.cong(Nat, Nat, z => Nat.add(7n, z), S, Nat.add(S, 0n), Equal.sym(Nat, Nat.add(S, 0n), S, N.add_zero(S))), Equal.trans(Nat, Nat.add(7n, Nat.add(S, 0n)), Nat.add(S, Nat.add(7n, 0n)), Nat.add(S, 7n), NA.add_swap(7n, S, 0n), {==})))), Equal.trans(Nat, Nat.add(Nat.add(S, 7n), Nat.add(S, 7n)), Nat.add(S, Nat.add(7n, Nat.add(S, 7n))), Nat.add(S, Nat.add(S, 14n)), NA.add_assoc(S, 7n, Nat.add(S, 7n)), Equal.cong(Nat, Nat, z => Nat.add(S, z), Nat.add(7n, Nat.add(S, 7n)), Nat.add(S, 14n), Equal.trans(Nat, Nat.add(7n, Nat.add(S, 7n)), Nat.add(S, Nat.add(7n, 7n)), Nat.add(S, 14n), NA.add_swap(7n, S, 7n), {==})))), Equal.sym(Nat, Nat.add(14n, Nat.add(S, S)), Nat.add(S, Nat.add(S, 14n)), Equal.trans(Nat, Nat.add(14n, Nat.add(S, S)), Nat.add(14n, Nat.add(S, Nat.add(S, 0n))), Nat.add(S, Nat.add(S, 14n)), Equal.cong(Nat, Nat, z => Nat.add(14n, z), Nat.add(S, S), Nat.add(S, Nat.add(S, 0n)), Equal.trans(Nat, Nat.add(S, S), Nat.add(Nat.add(S, 0n), Nat.add(S, 0n)), Nat.add(S, Nat.add(S, 0n)), Equal.trans(Nat, Nat.add(S, S), Nat.add(Nat.add(S, 0n), S), Nat.add(Nat.add(S, 0n), Nat.add(S, 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, S), 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), S, Nat.add(S, 0n), Equal.sym(Nat, Nat.add(S, 0n), S, N.add_zero(S)))), Equal.trans(Nat, Nat.add(Nat.add(S, 0n), Nat.add(S, 0n)), Nat.add(S, Nat.add(0n, Nat.add(S, 0n))), Nat.add(S, Nat.add(S, 0n)), NA.add_assoc(S, 0n, Nat.add(S, 0n)), Equal.cong(Nat, Nat, z => Nat.add(S, z), Nat.add(0n, Nat.add(S, 0n)), Nat.add(S, 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(S, 0n)), Nat.add(S, Nat.add(0n, 0n)), Nat.add(S, 0n), NA.add_swap(0n, S, 0n), {==}))))), Equal.trans(Nat, Nat.add(14n, Nat.add(S, Nat.add(S, 0n))), Nat.add(S, Nat.add(14n, Nat.add(S, 0n))), Nat.add(S, Nat.add(S, 14n)), NA.add_swap(14n, S, Nat.add(S, 0n)), Equal.cong(Nat, Nat, z => Nat.add(S, z), Nat.add(14n, Nat.add(S, 0n)), Nat.add(S, 14n), Equal.trans(Nat, Nat.add(14n, Nat.add(S, 0n)), Nat.add(S, Nat.add(14n, 0n)), Nat.add(S, 14n), NA.add_swap(14n, S, 0n), {==})))))))  +l1 = N.le_lt_succ(n, Nat.add(13n, Nat.add(S, S)), h)  +l2 = Equal.trans(Bool, Nat.is_le(Nat.add(7n, S), Nat.div(n, 2n)), Nat.is_le(Nat.mul(Nat.add(7n, S), 2n), n), False{}, NR.le_div(1n, Nat.add(7n, S), n), L.subst(Nat, z => {Nat.is_le(z, n) == False{} : Bool}, Nat.add(14n, Nat.add(S, S)), Nat.mul(Nat.add(7n, S), 2n), Equal.sym(Nat, Nat.mul(Nat.add(7n, S), 2n), Nat.add(14n, Nat.add(S, S)), e), N.lt_not_le(n, Nat.add(14n, Nat.add(S, S)), l1)))  N.lt_succ_le(Nat.div(n, 2n), Nat.add(6n, S), N.not_le_lt(Nat.add(7n, S), Nat.div(n, 2n), l2))