def add_double
bend-collections-laws-math@1.0.0.0 · proofs/lib/nat.bend:476
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as Nat
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)))