proposition: Lemma covers_permP s t : reflect (exists2 i : 'I_n0, s <R s * 's_i & t = s * 's_i) (covers s t).
proof: Proof. apply (iffP (coversP s t)). - move=> [/leperm_succ/= [i ltssi lessit Hsucc]]. exists i; first by []. move: lessit; rewrite le_eqVlt => /orP[/eqP ->// | ltssit]. exfalso; apply: (Hsucc (s * 's_i)). by rewrite ltssi ltssit. - move=> [/= i ltssi ->{t}]; split; first by []. move=> z /andP[/ltperm_length ltsz /ltperm_length]. move/leq_trans/(_ (lengthM s 's_i)); rewrite length_eltr addn1 ltnS. by move/(leq_trans ltsz); rewrite ltnn. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) permcomp tools permuted combclass congr presentSn ordtype