def mul_succ_right

bendtorch-core@0.1.0.0 · src/shape/nat_proofs.bend:52

import Base

52def mul_succ_right(+a: Nat, +q: Nat) -> {Nat.mul(a, 1n+q) == Nat.add(a, Nat.mul(a, q)) : Nat}:
53  match a:
54    case 0n:
55      {==}
56    case 1n+p:
57      %Equal.sym(Nat, Nat.mul(p, 1n+q), Nat.add(p, Nat.mul(p, q)), mul_succ_right(p, q)) : {1n+Nat.add(q, _) == 1n+Nat.add(p, Nat.add(q, Nat.mul(p, q))) : Nat}
58      %add_swap(q, p, Nat.mul(p, q)) : {1n+Nat.add(q, Nat.add(p, Nat.mul(p, q))) == 1n+_ : Nat}
59      {==}