proposition: Lemma perm_on_prods_length_ord s i (m : 'I_n) : i <= m -> perm_on [set k : 'I_n | k < m] s -> length (s * 's_[rev (iota (m - i) i)]) = length s + i.
proof: Proof. Proof using. elim: i s => [/= | i IHi] /= s Hm Hon; first by rewrite /= big_nil mulg1 addn0. rewrite rev_cons -cats1 big_cat /= {1}subnS prednK; last by rewrite subn_gt0. rewrite big_seq1 mulgA. have H : m - i.+1 < n0. rewrite -ltnS subnSK //; apply: (leq_trans _ (ltn_ord m)). by rewrite ltnS; exact: leq_subr. have:= H; rewrite -ltnS => /ltnW Ho. have -> : (m - i.+1) = Ordinal Ho by []. rewrite length_add1R //; first by rewrite (IHi _ (ltnW Hm) Hon) addnS {IHi}. have -> : Ordinal Ho = inord (m - i.+1) by apply val_inj => /=; rewrite inordK. rewrite invMg !permM inordK //. rewrite !subnS prednK; last by rewrite subn_gt0. rewrite {H Ho} prodsV invgK (prods_iota_mi (ltnW Hm)). have : m \notin [set k : 'I_n | k < m] by rewrite inE ltnn. move/(out_perm (perm_onV Hon)) ->. rewrite prods_iota_ltmi; first last. rewrite inordK; first by move: Hm; rewrite -subn_gt0; case: (m - i). apply: (leq_trans (leq_pred _)). by apply: (leq_trans (leq_subr _ _)); rewrite -ltnS. have:= perm_closed (inord (m - i).-1) (perm_onV Hon). rewrite !inE => -> /=; rewrite inordK. - rewrite prednK; last by rewrite subn_gt0. exact: leq_subr. - rewrite prednK; last by rewrite subn_gt0. by apply: (leq_trans (leq_subr _ _)); exact: ltnW. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr