proposition: Lemma enum_inord (m : nat) : enum 'I_m.+1 = [seq inord i | i <- iota 0 m.+1].
proof: Proof. rewrite -val_enum_ord -map_comp. transitivity ([seq i | i <- enum 'I_m.+1]); first by rewrite map_id. apply eq_map => i /=; by rewrite inord_val. Qed.
imports: mathcomp(all_ssreflect fingroup perm)