def mul_succ

bend-collections-laws-math@1.0.0.0 · proofs/lib/lemmas/proofs/nat_algebra.bend:41

import Base

41def mul_succ(a: Nat, +b: Nat) -> {Nat.mul(a, 1n+b) == Nat.add(a, Nat.mul(a, b)) : Nat}:
42  match a:
43    case 0n: {==}
44    case 1n++p:
45      %Equal.sym(Nat, Nat.mul(p, 1n+b), Nat.add(p, Nat.mul(p, b)), mul_succ(p, b)) : {1n+Nat.add(b, _) == 1n+Nat.add(p, Nat.add(b, Nat.mul(p, b))) : Nat}
46      succ_equal(Nat.add(b, Nat.add(p, Nat.mul(p, b))), Nat.add(p, Nat.add(b, Nat.mul(p, b))), add_swap(b, p, Nat.mul(p, b)))