d : Nat
n : Int
a : Nat
d0 : d ≠ 0
a0 : a ≠ 0
⊢ normalize (n * ↑a) (d * a) = normalize (↑a * n) (a * d)
d : Nat
n : Int
a : Nat
d0 : d ≠ 0
a0 : a ≠ 0
⊢ normalize (n * ↑a) (d * a) = normalize n d
rw [← normalize_mul_left (d0 := d0) a0]
no goals
d : Nat
n : Int
a : Nat
d0 : d ≠ 0
a0 : a ≠ 0
⊢ normalize (n * ↑a) (d * a) = normalize (↑a * n) (a * d)
congr 1 <;> [apply Int.mul_comm; apply Nat.mul_comm]