def nw_prod

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64sqn.bend:40
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqn.bend as F64sqn
import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as NR
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as FR

40# the product bound: (1 + S)^2 <= c3 * r0 when c3 + d = S + 14 and d^2 + 1 <= 12 S
41def 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}:
42  +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))))))
43  +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))))))))
44  +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))
45  +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)))))))))))
46  +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))
47  +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))))))))
48  +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))
49  +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))))))
50  +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)))))
51  +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)
52  +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)
53  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)
Uses (24)

Used by (1)

bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqn:nw_hi