conv at this => dsimp; rewrite [← mul_assoc, inv_mul, one_mul]
n : Nat
x y z : Permutation n
h : y * x = z
this : (fun x => inv y * x) (y * x) = (fun x => inv y * x) z
⊢ x = inv y * z
n : Nat
x y z : Permutation n
h : y * x = z
this : x = inv y * z
⊢ x = inv y * z