def dbl_add

bend-collections-laws-crypto@1.0.0.0 · proofs/math/random/lemire.bend:240

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N

240def dbl_add(+z: Nat) -> {Nat.double(z) == Nat.add(z, z) : Nat}:
241  match z:
242    case 0n:
243      {==}
244    case 1n+p:
245      %Equal.sym(Nat, Nat.add(p, 1n+p), 1n+Nat.add(p, p), N.add_succ(p, p)) : {2n+Nat.double(p) == 1n+_ : Nat}
246      Equal.cong(Nat, Nat, x => 2n+x, Nat.double(p), Nat.add(p, p), dbl_add(p))