def mul_sub_left

bend-collections-laws-math@1.0.0.0 · proofs/math/natural/fact.bend:163

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as A
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as R

163# a (x - y) == a x - a y
164def mul_sub_left(+a: Nat, +x: Nat, +y: Nat) -> {Nat.mul(a, Nat.sub(x, y)) == Nat.sub(Nat.mul(a, x), Nat.mul(a, y)) : Nat}:
165  %Equal.sym(Nat, Nat.mul(a, Nat.sub(x, y)), Nat.mul(Nat.sub(x, y), a), A.mul_comm(a, Nat.sub(x, y))) : {_ == Nat.sub(Nat.mul(a, x), Nat.mul(a, y)) : Nat}
166  %Equal.sym(Nat, Nat.mul(a, x), Nat.mul(x, a), A.mul_comm(a, x)) : {Nat.mul(Nat.sub(x, y), a) == Nat.sub(_, Nat.mul(a, y)) : Nat}
167  %Equal.sym(Nat, Nat.mul(a, y), Nat.mul(y, a), A.mul_comm(a, y)) : {Nat.mul(Nat.sub(x, y), a) == Nat.sub(Nat.mul(x, a), _) : Nat}
168  R.mul_sub(x, y, a)