law double_eq_add

bend-mathlib@0.8.1.0 · nat.bend:1252

import Base

1252# Doubling is adding a natural to itself.
1253law double_eq_add:
1254  for n: Nat
1255  {Nat.double(n) == Nat.add(n, n) : Nat}