def mul_sub

bend-collections-laws-math@1.0.0.0 · proofs/math/natural/arith.bend:104

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

104# (x - y) c == x c - y c   (Mathlib Nat.mul_sub_right_distrib)
105def 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}:
106  match x y:
107    case 0n 0n:
108      {==}
109    case 0n 1n+ +yp:
110      Equal.sym(Nat, Nat.sub(0n, Nat.add(c, Nat.mul(yp, c))), 0n, zsub(Nat.add(c, Nat.mul(yp, c))))
111    case 1n+ +xp 0n:
112      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))))
113    case 1n+ +xp 1n+ +yp:
114      %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}
115      mul_sub(xp, yp, c)