F64addg.rca: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addg.bend as F64addg
Lines 118-122 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addg.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addg.bend&start_line=118&end_line=122

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as SF
import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L

def rca(+s: Bool, +a: Nat, +a2: Nat, +ha: {a == a2 : Nat}, +k: Nat, +k2: Nat, +hk: {k == k2 : Nat}, +m: Nat, +m2: Nat, +hm: {m == m2 : Nat}, +x: Nat, +x2: Nat, +hx: {x == x2 : Nat}) -> {SF.round(s, Nat.add(a, C.shift(k, m)), x) == SF.round(s, Nat.add(a2, C.shift(k2, m2)), x2) : F.F64}:
  +e1 = L.subst(Nat, z => {SF.round(s, Nat.add(a, C.shift(k, m)), x) == SF.round(s, Nat.add(z, C.shift(k, m)), x) : F.F64}, a, a2, ha, {==})
  +e2 = L.subst(Nat, z => {SF.round(s, Nat.add(a, C.shift(k, m)), x) == SF.round(s, Nat.add(a2, C.shift(z, m)), x) : F.F64}, k, k2, hk, e1)
  +e3 = L.subst(Nat, z => {SF.round(s, Nat.add(a, C.shift(k, m)), x) == SF.round(s, Nat.add(a2, C.shift(k2, z)), x) : F.F64}, m, m2, hm, e2)
  L.subst(Nat, z => {SF.round(s, Nat.add(a, C.shift(k, m)), x) == SF.round(s, Nat.add(a2, C.shift(k2, m2)), z) : F.F64}, x, x2, hx, e3)

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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=bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend&name=subst
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=shift
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=round
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=F64