proposition: Lemma length_descR s (i : 'I_n) : i < n0 -> (s^-1 i < s^-1 (inord i.+1)) = (length (s * 's_i) > length s).
proof: Proof. Proof using. by move/length_descL ->; rewrite -{1}eltrV -invMg !lengthV. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr