proposition: Lemma length_descL s (i : 'I_n) : i < n0 -> (s i < s (inord i.+1)) = (length ('s_i * s) > length s).
proof: Proof. Proof using. move=> Hi. case: (ltngtP (s i) (s (inord i.+1))) => Hsi; apply esym. - by rewrite (length_add1L Hi Hsi) ltnS leqnn. - by rewrite (length_sub1L Hi Hsi) ltnNge leqnSn. - exfalso; move/val_inj/perm_inj/(congr1 val)/eqP: Hsi. by rewrite /= inordK ?ltnS // trivSimpl. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr