proposition: Lemma prods_iota_mi (m : 'I_n) i : i <= m -> 's_[iota (m - i) i] (inord (m - i)) = m.
proof: Proof. Proof using. elim: i => [| i IHi] /= Hm. by rewrite subn0 inord_val big_nil perm1. rewrite big_cons permM eltrL. rewrite subnS prednK; last by rewrite subn_gt0. by apply: IHi; exact: ltnW. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr