def mul_swap

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/semiring.bend:21

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

21def mul_swap(+a: Nat, +b: Nat, +c: Nat) -> {Nat.mul(a, Nat.mul(b, c)) == Nat.mul(b, Nat.mul(a, c)) : Nat}:
22  %NA.mul_assoc(a, b, c) : {_ == Nat.mul(b, Nat.mul(a, c)) : Nat}
23  %NA.mul_assoc(b, a, c) : {Nat.mul(Nat.mul(a, b), c) == _ : Nat}
24  %NA.mul_comm(a, b) : {Nat.mul(Nat.mul(a, b), c) == Nat.mul(_, c) : Nat}
25  {==}