law double_add

bend-mathlib@0.8.1.0 · nat.bend:3555

import Base

3555# Doubling distributes over addition: double (a + b) = double a + double b.
3556law double_add:
3557  for a: Nat
3558  for b: Nat
3559  {Nat.double(Nat.add(a, b)) == Nat.add(Nat.double(a), Nat.double(b)) : Nat}