law double_add_sym

bend-mathlib@0.8.1.0 · nat.bend:4801

import Base

4801# Doubling distributes over addition: double (a + b) = double a + double b, reversed to rewrite toward the simple side.
4802law double_add_sym:
4803  for a: Nat
4804  for b: Nat
4805  {Nat.add(Nat.double(a), Nat.double(b)) == Nat.double(Nat.add(a, b)) : Nat}