Theorem: LoVe.Nat.two_mul (LoVe/LoVelib.lean)

State before:
n : ℕ
⊢ 2 * n = n + n
Tactic:
ring
State after:
no goals