proposition: Theorem eltr_ind (P : 'S_n -> Type) : P 1 -> (forall s i, i < n0 -> P s -> P ('s_i * s)) -> forall s, P s.
proof: Proof. Proof using. move=> H1 IH s; rewrite -(canwordP s). elim: (canword s) => [| t0 t IHt] /=; first by rewrite big_nil. by rewrite big_cons; apply IH; first exact: ltn_ord. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr