proposition: Lemma rho_iota : rho = rev (iota 0 n) :> seq nat.
proof: Proof. Proof using. apply (eq_from_nth (x0 := 0%N)). by rewrite size_rev size_iota size_map size_enum_ord. move=> i; rewrite size_map size_enum_ord => Hi. rewrite nth_rev size_iota // (nth_map (Ordinal Hi)); last by rewrite size_enum_ord. rewrite nth_enum_ord // nth_iota; first last. by case: n Hi => [// | m] _; rewrite ltnS subSS; apply: leq_subr. by rewrite add0n; case: n Hi => [// | m] _; rewrite !subSS subn0. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition