Predicate for an element being an inverse in a comm_monoid

Stream: Is there code for X?

[Chris Hughes]

Do we have a predicate for x * y = 1 when x and y are in a comm_monoid with lemmas like x ^ n * y ^ n = 1?

[Anne Baanen]

Something like docs#invertible but with a given inverse?

[Yaël Dillies]

There's docs#is_left_inv, but I fear there's no API for it

[Chris Hughes]

I'll just use the hypothesis x * y = 1 in that case. Just checking if there's a correct way of stating this.

[Chris Hughes]

ACtually invertible looks like what I want