def add_double

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/nat.bend:476

import Base

476def add_double(+a: Nat, +b: Nat) -> {Nat.add(Nat.double(a), Nat.double(b)) == Nat.double(Nat.add(a, b)) : Nat}:
477  match a:
478    case 0n:
479      {==}
480    case 1n+p:
481      succ_cong(1n+Nat.add(Nat.double(p), Nat.double(b)), 1n+Nat.double(Nat.add(p, b)), succ_cong(Nat.add(Nat.double(p), Nat.double(b)), Nat.double(Nat.add(p, b)), add_double(p, b)))