Arith.mul_sub: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as Arith
Lines 104-115 of bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend&start_line=104&end_line=115

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N

# (x - y) c == x c - y c   (Mathlib Nat.mul_sub_right_distrib)
def mul_sub(+x: Nat, +y: Nat, +c: Nat) -> {Nat.mul(Nat.sub(x, y), c) == Nat.sub(Nat.mul(x, c), Nat.mul(y, c)) : Nat}:
  match x y:
    case 0n 0n:
      {==}
    case 0n 1n+ +yp:
      Equal.sym(Nat, Nat.sub(0n, Nat.add(c, Nat.mul(yp, c))), 0n, zsub(Nat.add(c, Nat.mul(yp, c))))
    case 1n+ +xp 0n:
      Equal.sym(Nat, Nat.sub(Nat.add(c, Nat.mul(xp, c)), 0n), Nat.add(c, Nat.mul(xp, c)), N.sub_zero(Nat.add(c, Nat.mul(xp, c))))
    case 1n+ +xp 1n+ +yp:
      %Equal.sym(Nat, Nat.sub(Nat.add(c, Nat.mul(xp, c)), Nat.add(c, Nat.mul(yp, c))), Nat.sub(Nat.mul(xp, c), Nat.mul(yp, c)), sub_cancel_l(c, Nat.mul(xp, c), Nat.mul(yp, c))) : {Nat.mul(Nat.sub(xp, yp), c) == _ : Nat}
      mul_sub(xp, yp, c)

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=sub_zero
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend&name=sub_cancel_l
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend&name=zsub