def dbl

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u32laws.bend:179

import Base

179def dbl(+h: Nat) -> {Nat.mul(h, 2n) == Nat.double(h) : Nat}:
180  match h:
181    case 0n:
182      {==}
183    case 1n+ +p:
184      %Equal.sym(Nat, Nat.mul(p, 2n), Nat.double(p), dbl(p)) : {Nat.add(2n, _) == Nat.double(1n+p) : Nat}
185      {==}