~/jendhub

def mul_swap

bendtorch-core@0.1.0.0 · src/tensor/signed_PROOF.bend:487

import bendtorch-core@0.1.0.0/src/tensor/signed_PROOF.bend as SignedPROOF
import Base
import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as NatProofs

487# e * (s * p) = s * (e * p).
488def mul_swap(+e: Nat, +s: Nat, +p: Nat) -> {Nat.mul(e, Nat.mul(s, p)) == Nat.mul(s, Nat.mul(e, p)) : Nat}:
489  Equal.trans(Nat, Nat.mul(e, Nat.mul(s, p)), Nat.mul(Nat.mul(e, s), p), Nat.mul(s, Nat.mul(e, p)),
490    Equal.sym(Nat, Nat.mul(Nat.mul(e, s), p), Nat.mul(e, Nat.mul(s, p)), NatProofs.mul_assoc(e, s, p)),
491    Equal.trans(Nat, Nat.mul(Nat.mul(e, s), p), Nat.mul(Nat.mul(s, e), p), Nat.mul(s, Nat.mul(e, p)),
492      Equal.cong(Nat, Nat, x => Nat.mul(x, p), Nat.mul(e, s), Nat.mul(s, e), NatProofs.mul_comm(e, s)),
493      NatProofs.mul_assoc(s, e, p)))

Uses (7)

Used by (1)