Theorem: Pos.right_distrib (Extra/Pos/Lemmas.lean)

State before:
x y z : Pos
⊢ (x + y) * z = x * z + y * z
Tactic:
by_toNat
State after:
x y z : Pos
⊢ (x.toNat + y.toNat) * z.toNat = x.toNat * z.toNat + y.toNat * z.toNat

State before:
x y z : Pos
⊢ (x.toNat + y.toNat) * z.toNat = x.toNat * z.toNat + y.toNat * z.toNat
Tactic:
exact Nat.right_distrib ..
State after:
no goals