law mul_two_sym

bend-mathlib@0.8.1.0 · nat.bend:4875

import Base

4875# Multiplying n by two gives n + n, reversed to rewrite toward the simple side.
4876law mul_two_sym:
4877  for n: Nat
4878  {Nat.add(n, n) == Nat.mul(n, 2n) : Nat}