Theorem: Misc.Nat.eq_one_of_mul_eq_one_left (LeanSAT/Util/Misc.lean)

State before:
m n : Nat
H : m * n = 1
⊢ n * ?m.11360 = 1
Tactic:
rwa [Nat.mul_comm]
State after:
no goals