def mm_swap

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/top.bend:31

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

31def mm_swap(+p: Nat, +x: Nat) -> {Nat.mul(Nat.mul(4n, p), x) == Nat.mul(Nat.mul(4n, x), p) : Nat}:
32  Equal.trans(Nat, Nat.mul(Nat.mul(4n, p), x), Nat.mul(4n, Nat.mul(p, x)), Nat.mul(Nat.mul(4n, x), p),
33    NA.mul_assoc(4n, p, x),
34    Equal.trans(Nat, Nat.mul(4n, Nat.mul(p, x)), Nat.mul(4n, Nat.mul(x, p)), Nat.mul(Nat.mul(4n, x), p),
35      Equal.cong(Nat, Nat, z => Nat.mul(4n, z), Nat.mul(p, x), Nat.mul(x, p), NA.mul_comm(p, x)),
36      Equal.sym(Nat, Nat.mul(Nat.mul(4n, x), p), Nat.mul(4n, Nat.mul(x, p)), NA.mul_assoc(4n, x, p))))