proposition: Lemma size_straighten w : size (straighten w) = n.+1.
proof: Proof. Proof using. rewrite /straighten; elim/last_ind: w => [| w wn IHw] //=. by rewrite size_nseq. by rewrite rev_rcons /= size_inscode. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr