I can see a way to try to prove this by cutting `s`

into pieces, using `i1`

and `i2`

as boundaries, but before diving into this, I wonder whether there is more elegant way to prove this:

```
lt1s : i1 < size s
lt2s : i2 < size s
============================
perm_eq [seq (if i == i2 then i1 else if i == i1 then i2 else i) | i <- iota 0 (size s)]
(iota 0 (size s))
```

Maybe using `set_nth`

?

Ah, I hadn't considered this approach. Thanks for the idea :smile:

I think that relying on the definition of `perm_eq`

or using `permP`

is the easiest way to prove that. https://math-comp.github.io/htmldoc/mathcomp.ssreflect.seq.html#perm_eq

Indeed, and if you use `set_nth`

, this PR may be useful: https://github.com/math-comp/math-comp/pull/877

While thinking about all these interesting suggestions, I also figured out that using `uniq_perm`

led to a somewhat short proof, using `map_uniq`

and the fact that a transposition is an involution to prove the unicity of the transposed `iota`

.

Last updated: Jul 15 2024 at 21:02 UTC