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