def g3

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64rint.bend:95

import Base
import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F

95def g3(+m: F.RMode, +s: Bool, +a: Nat, +a2: Nat, +ha: {a == a2 : Nat}, +b: Nat, +b2: Nat, +hb: {b == b2 : Nat}, +c: Nat, +c2: Nat, +hc: {c == c2 : Nat}) -> {G(m, s, a, b, c) == G(m, s, a2, b2, c2) : F.F64}:
96  +e1 = Equal.cong(Nat, F.F64, t => G(m, s, t, b, c), a, a2, ha)
97  +e2 = Equal.cong(Nat, F.F64, t => G(m, s, a2, t, c), b, b2, hb)
98  +e3 = Equal.cong(Nat, F.F64, t => G(m, s, a2, b2, t), c, c2, hc)
99  Equal.trans(F.F64, G(m, s, a, b, c), G(m, s, a2, b, c), G(m, s, a2, b2, c2), e1, Equal.trans(F.F64, G(m, s, a2, b, c), G(m, s, a2, b2, c), G(m, s, a2, b2, c2), e2, e3))