law double_eq_add_sym

bend-mathlib@0.8.1.0 · nat.bend:4231

import Base

4231# Doubling is adding a natural to itself, reversed to rewrite toward the simple side.
4232law double_eq_add_sym:
4233  for n: Nat
4234  {Nat.add(n, n) == Nat.double(n) : Nat}