proposition: Lemma eq_inv_std (u : seq T) : eq_inv u (std u).
proof: Proof. move Hn : (size u) => n. elim: n u Hn => [| n IHn] u Hn. move: Hn => /eqP/nilP ->. by rewrite /std /=; apply: eq_inv_nil. case Hu : u Hn => [// | u0 u']; rewrite -Hu => Hn. have Hszrem : size (rembig u) = n by rewrite size_rembig Hn. move/(_ (rembig u) Hszrem) : IHn. rewrite /std Hn /= Hszrem => /eq_invP[_ Hinv]. apply/eq_invP; split. by rewrite size_cat /= addnS -size_cat cat_take_drop size_std_rec. move=> i j /andP[Hij Hj]. rewrite {1 2}[u]Hu -posbig_take_dropE -Hu. have Hpossz : posbig u <= size (rembig u). have /posbig_size : u != [::] by rewrite Hu. by rewrite Hszrem Hn. rewrite !(nth_inspos _ _ _ Hpossz). have Hposszstd : posbig u <= size (std_rec n (rembig u)). by rewrite size_std_rec -Hszrem. rewrite !(nth_inspos _ _ _ Hposszstd). case/altP: (i =P posbig u) => Hipos. - subst i. case/altP: (j =P posbig u) => Hjpos; first by rewrite !lexx. rewrite -nth_rembig (shiftinv_posK Hjpos). have {Hij}Hjpos : posbig u < j by rewrite ltn_neqAle eq_sym Hij Hjpos. have /allP Hall := allLtn_std_rec (rembig u). set uj := (X in (n <= X)%O). have /Hall /= : uj \in std (rembig u). rewrite /std Hszrem. apply: mem_nth; rewrite /shiftinv_pos size_std_rec [j < _]ltnNge (ltnW Hjpos) /=. move: Hjpos Hj; case j => [// |j'] /= _. by rewrite Hn. rewrite Hszrem [(n <= uj)%O]leNgt => -> /= {Hall uj}. rewrite -(subnKC Hjpos) -nth_drop. have:= allLtn_posbig u0 u'; rewrite -Hu => /allP /= Hall. set uj := (X in (_ <= X)%O). have /Hall /= : uj \in drop (posbig u).+1 u. apply: mem_nth; rewrite size_drop ltn_sub2r //=. exact: (leq_ltn_trans Hjpos). by rewrite leNgt => ->. - case/altP: (j =P posbig u) => Hjpos. + subst j. have {Hij}Hipos : i < posbig u by rewrite ltn_neqAle Hipos Hij. rewrite /shiftinv_pos Hipos -nth_rembig. have /allP Hall := maxLP u0 u'. set ui := (nth _ _ _). have {ui} {}/Hall /= -> : ui \in (u0 :: u'). rewrite /ui Hu; apply: mem_nth. rewrite /shift_pos -Hu Hipos. exact: (ltn_trans Hipos). have:= allLtn_std_rec (rembig u) => /allP Hall. set ui := (nth _ _ _). have /Hall /= : ui \in std (rembig u). rewrite /std Hszrem. apply: mem_nth; rewrite /shiftinv_pos size_std_rec -Hszrem. exact: (leq_trans Hipos). by rewrite Hszrem => /ltW ->. + apply: Hinv; rewrite (shiftinv_pos_homo _ Hij) /=. rewrite /shiftinv_pos. case (ltnP j (posbig u)) => Hjpos2; first exact: (leq_trans Hjpos2). have {Hjpos Hjpos2} : posbig u < j by rewrite ltn_neqAle eq_sym Hjpos2 Hjpos. case: j Hj {Hij} => [// | j] /=. by rewrite Hn Hszrem ltnS. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp