~/jendhub

def cmul

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/poly1305/arith.bend:25

import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/arith.bend as Arith
import Base

25def cmul(+a: Nat, +a2: Nat, +b: Nat, +b2: Nat, +ea: {a == a2 : Nat}, +eb: {b == b2 : Nat}) -> {Nat.mul(a, b) == Nat.mul(a2, b2) : Nat}:
26  tr(Nat.mul(a, b), Nat.mul(a2, b), Nat.mul(a2, b2), Equal.cong(Nat, Nat, t => Nat.mul(t, b), a, a2, ea), Equal.cong(Nat, Nat, t => Nat.mul(a2, t), b, b2, eb))

Uses (4)

Used by (1)