proposition: Lemma perm_on_prods_length s i m : m < 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. move=> Hm; rewrite -[m]/(val (Ordinal Hm)). exact: perm_on_prods_length_ord. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr