law mul_two

bend-mathlib@0.8.1.0 · nat.bend:3754

import Base

3754# Multiplying n by two gives n + n.
3755law mul_two:
3756  for n: Nat
3757  {Nat.mul(n, 2n) == Nat.add(n, n) : Nat}