no goals
M : Type ?u.7068
N : Type u_1
μ : M → N → N
r : N → N → Prop
inst✝ : CommSemigroup N
⊢ Contravariant N N (flip fun x x_1 => x * x_1) r ↔ Contravariant N N (fun x x_1 => x * x_1) r
rw [flip_mul]