F64sqk.sqa: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqk.bend as F64sqk
Lines 17-19 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqk.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqk.bend&start_line=17&end_line=19

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA

# (a + b)^2 expanded
def sqa(+a: Nat, +b: Nat) -> {Nat.mul(Nat.add(a, b), Nat.add(a, b)) == Nat.add(Nat.add(Nat.mul(a, a), Nat.add(Nat.mul(a, b), Nat.mul(a, b))), Nat.mul(b, b)) : Nat}:
  Equal.trans(Nat, Nat.mul(Nat.add(a, b), Nat.add(a, b)), Nat.add(Nat.mul(a, Nat.add(a, b)), Nat.mul(b, Nat.add(a, b))), Nat.add(Nat.add(Nat.mul(a, a), Nat.add(Nat.mul(a, b), Nat.mul(a, b))), Nat.mul(b, b)), NA.mul_add_right(a, b, Nat.add(a, b)), Equal.trans(Nat, Nat.add(Nat.mul(a, Nat.add(a, b)), Nat.mul(b, Nat.add(a, b))), Nat.add(Nat.add(Nat.mul(a, a), Nat.mul(a, b)), Nat.mul(b, Nat.add(a, b))), Nat.add(Nat.add(Nat.mul(a, a), Nat.add(Nat.mul(a, b), Nat.mul(a, b))), Nat.mul(b, b)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.mul(b, Nat.add(a, b))), Nat.mul(a, Nat.add(a, b)), Nat.add(Nat.mul(a, a), Nat.mul(a, b)), NA.mul_add_left(a, a, b)), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(a, a), Nat.mul(a, b)), Nat.mul(b, Nat.add(a, b))), Nat.add(Nat.add(Nat.mul(a, a), Nat.mul(a, b)), Nat.add(Nat.mul(b, a), Nat.mul(b, b))), Nat.add(Nat.add(Nat.mul(a, a), Nat.add(Nat.mul(a, b), Nat.mul(a, b))), Nat.mul(b, b)), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.mul(a, a), Nat.mul(a, b)), z), Nat.mul(b, Nat.add(a, b)), Nat.add(Nat.mul(b, a), Nat.mul(b, b)), NA.mul_add_left(b, a, b)), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(a, a), Nat.mul(a, b)), Nat.add(Nat.mul(b, a), Nat.mul(b, b))), Nat.add(Nat.add(Nat.mul(a, a), Nat.mul(a, b)), Nat.add(Nat.mul(a, b), Nat.mul(b, b))), Nat.add(Nat.add(Nat.mul(a, a), Nat.add(Nat.mul(a, b), Nat.mul(a, b))), Nat.mul(b, b)), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.mul(a, a), Nat.mul(a, b)), Nat.add(z, Nat.mul(b, b))), Nat.mul(b, a), Nat.mul(a, b), NA.mul_comm(b, a)), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(a, a), Nat.mul(a, b)), Nat.add(Nat.mul(a, b), Nat.mul(b, b))), Nat.add(Nat.mul(a, a), Nat.add(Nat.mul(a, b), Nat.add(Nat.mul(a, b), Nat.mul(b, b)))), Nat.add(Nat.add(Nat.mul(a, a), Nat.add(Nat.mul(a, b), Nat.mul(a, b))), Nat.mul(b, b)), NA.add_assoc(Nat.mul(a, a), Nat.mul(a, b), Nat.add(Nat.mul(a, b), Nat.mul(b, b))), Equal.trans(Nat, Nat.add(Nat.mul(a, a), Nat.add(Nat.mul(a, b), Nat.add(Nat.mul(a, b), Nat.mul(b, b)))), Nat.add(Nat.mul(a, a), Nat.add(Nat.add(Nat.mul(a, b), Nat.mul(a, b)), Nat.mul(b, b))), Nat.add(Nat.add(Nat.mul(a, a), Nat.add(Nat.mul(a, b), Nat.mul(a, b))), Nat.mul(b, b)), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(a, a), z), Nat.add(Nat.mul(a, b), Nat.add(Nat.mul(a, b), Nat.mul(b, b))), Nat.add(Nat.add(Nat.mul(a, b), Nat.mul(a, b)), Nat.mul(b, b)), Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(a, b), Nat.mul(a, b)), Nat.mul(b, b)), Nat.add(Nat.mul(a, b), Nat.add(Nat.mul(a, b), Nat.mul(b, b))), NA.add_assoc(Nat.mul(a, b), Nat.mul(a, b), Nat.mul(b, b)))), Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(a, a), Nat.add(Nat.mul(a, b), Nat.mul(a, b))), Nat.mul(b, b)), Nat.add(Nat.mul(a, a), Nat.add(Nat.add(Nat.mul(a, b), Nat.mul(a, b)), Nat.mul(b, b))), NA.add_assoc(Nat.mul(a, a), Nat.add(Nat.mul(a, b), Nat.mul(a, b)), Nat.mul(b, b)))))))))

Uses (10):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_assoc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=mul_add_left
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=mul_add_right
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=mul_comm