proposition: Lemma prods_iota_ltmi i (m u : 'I_n) : u < m - i -> 's_[(iota (m - i) i)] u = u.
proof: Proof. Proof using. rewrite big_seq=> ltumi; elim/big_ind: _ => /=. - by rewrite perm1. - by move=> s t Hs Ht; rewrite permM Hs Ht. move=> j; rewrite mem_iota. case: (ltnP m i) => [/ltnW | /subnK->]. by rewrite -subn_eq0 => /eqP H; rewrite H in ltumi. move=> /andP[/(leq_trans ltumi) ltuj /leq_ltn_trans/(_ (ltn_ord _)) ltjn1]. have jo := ltn_trans (ltnSn _) ltjn1. rewrite eltrD // -val_eqE //= inordK // gtn_eqF //. exact: (ltn_trans ltuj (ltnSn _)). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr