proposition: Lemma map_nth_iota_id l : map (nth a l) (iota 0 (size l)) = l.
proof: Proof. apply: (@eq_from_nth _ a); first by rewrite size_map size_iota. rewrite size_map; move=> i; rewrite size_iota => Hi. by rewrite (@nth_map _ 0 _ _ _ _ _) // ?size_iota // nth_iota. Qed.
imports: mathcomp(all_ssreflect fingroup perm)