proposition: Lemma invset_eltrL s (i : 'I_n) : i < n0 -> s i < s (inord i.+1) -> invset ('s_i * s) = (i, inord i.+1) |: [set ('s_i p.1, 's_i p.2) | p in invset s].
proof: Proof. move => Hi Hfwd. apply/setP => [/= [u v]] /=; rewrite !inE /= !permM. apply/idP/idP. - move=> /andP[Huv]. case: tpermP => /= [Hv | Hv | /eqP Hvi /eqP Hvi1]. + rewrite inord_val in Hv; subst v. have Htu : 's_i u = u. rewrite eltrD // eq_sym. * by move: Huv; apply contraL => /eqP ->; rewrite ltnn. * by move: Huv; apply contraL => /eqP ->; rewrite /= -leqNgt inordi1. rewrite Htu => Hs; apply/orP; right. apply/imsetP; exists (u, inord i.+1); first last. by rewrite /= eltrR Htu. by rewrite inE /= Hs andbT inordi1 //; apply/(ltn_trans Huv). + rewrite inord_val; subst v; case: tpermP. * by move=> ->; rewrite inord_val eq_refl. * by move=> Hu; move: Huv; rewrite Hu ltnn. rewrite inord_val => /eqP Hiu /eqP Hi1u. have Htu : 's_i u = u by rewrite eltrD // eq_sym. move=> Hsiu; apply/orP; right. apply/imsetP; exists (u, i); last by rewrite Htu /= eltrL. by rewrite inE /= Hsiu andbT ltn_neqAle Hiu -ltnS -(inordi1 Hi) Huv. rewrite inord_val in Hvi. case: tpermP => [Hu | Hu | /eqP Hui /eqP Hui1]. + rewrite inord_val in Hu; subst u => Hsvi1. have Htv : 's_i v = v by rewrite eltrD // eq_sym. apply/orP; right. apply/imsetP; exists ((inord i.+1), v); last by rewrite Htv /= eltrR. rewrite inE /= Hsvi1 ltn_neqAle inordi1 //. by rewrite Huv !andbT eq_sym -(inordi1 Hi) Hvi1. + rewrite inord_val; subst u => Hsvi1. have Htv : 's_i v = v by rewrite eltrD // eq_sym // inord_val. apply/orP; right. apply/imsetP; exists (i, v); last by rewrite Htv /= eltrL. rewrite inE /= Hsvi1 ltn_neqAle eq_sym Hvi !andbT /=. by move: Huv; rewrite inordi1 // => /ltnW/ltnW. + rewrite inord_val in Hui; move=> Hsvu. apply/orP; right. apply/imsetP; exists (u, v); last by rewrite !eltrD // eq_sym. by rewrite inE /= Huv Hsvu. - move/orP => [/eqP[->{u} ->{v}] | /imsetP[[/= a b]]]. by rewrite eltrL eltrR Hfwd inordi1 // ltnS leqnn. rewrite inE /= => /andP[Hab Hsba] [->{u} ->{v}]. rewrite !eltrK Hsba andbT (eltr_exchange Hi Hab) -negb_and. move: Hsba; apply contraL; rewrite -leqNgt => /andP[/eqP/val_inj<- /eqP Hib]. have -> : b = (inord i.+1) by apply val_inj; rewrite /= -Hib inordi1. exact: ltnW. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr