no goals
α : Type ?u.81558
m p : PosNum
⊢ ↑(m * p) + ↑(m * p) = ↑m * (↑p + ↑p)
rw [mul_to_nat m p, left_distrib]
no goals
α : Type ?u.81558
m p : PosNum
⊢ ↑(m * p) + ↑(m * p) + ↑m = ↑m * (↑p + ↑p) + ↑m
rw [mul_to_nat m p, left_distrib]