def double_self

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/lemmas/proofs/nat_algebra.bend:83

import Base

83def double_self(n: Nat) -> {Nat.double(n) == Nat.add(n, n) : Nat}:
84  match n:
85    case 0n: {==}
86    case 1n++p:
87      %Equal.sym(Nat, Nat.double(p), Nat.add(p, p), double_self(p)) : {2n+_ == 1n+Nat.add(p, 1n+p) : Nat}
88      succ_equal(1n+Nat.add(p, p), Nat.add(p, 1n+p), Equal.sym(Nat, Nat.add(p, 1n+p), 1n+Nat.add(p, p), add_succ(p, p)))