def mul_one_right

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

import Base

68def mul_one_right(+a: Nat) -> {Nat.mul(a, 1n) == a : Nat}:
69  match a:
70    case 0n:
71      {==}
72    case 1n+p:
73      Equal.cong(Nat, Nat, value => 1n+value, Nat.mul(p, 1n), p, mul_one_right(p))