How can I formulate the rearrangement theorem [1] and then prove it, by coq?

[1] https://mathworld.wolfram.com/RearrangementTheorem.html

Regards

HZ

There are several ways to formulate this property.

Maybe one that is close enough to Wolfram formulation is

```
From mathcomp Require Import all_ssreflect all_fingroup.
Variable gT : finGroupType.
Variable G : {group gT}.
Lemma rearrangement x :
x \in G -> perm_eq [seq i | i in G] [seq (x * i)%g | i in G].
```

it requires some expertise about `perm_eq`

to prove but it is a consequence of the theorem `mulgI`

.

Last updated: Jul 15 2024 at 21:02 UTC