proposition: Lemma predi_eltrp p : i < n -> predi p -> predi (eltrp p).
proof: Proof. Proof using. move=> Hi. have Hii1 : val (@inord n i.+1) = (@inord n i).+1. by do 2 (rewrite /= inordK; last by apply (leq_trans Hi)). move: p => [u v] /=; rewrite /predi /= /eltrp => /andP[Hlt Hneq] /=. case/altP: (inord i =P u) => Hu. subst u; rewrite eltrL. case/altP: (v =P inord i.+1) Hneq Hlt => [Hu | Hu _ Hlt]. by subst v; rewrite /= eq_refl. rewrite eltrD; [| by rewrite neq_ltn Hlt | by rewrite eq_sym]. apply/andP; split. - by rewrite ltn_neqAle eq_sym Hu /= Hii1. - rewrite /eq_op /= eq_sym; apply/nandP; left. by rewrite /eq_op /= Hii1 ieqi1F. case/altP: (inord i.+1 =P u) => Hu1. subst u; rewrite eltrR /=. rewrite eltrD; first last. - by move: Hlt; rewrite ltn_neqAle => /andP[]. - move: Hlt; rewrite Hii1 => /ltnW. by rewrite ltn_neqAle => /andP[]. apply/andP; split. - by apply: (ltn_trans _ Hlt); rewrite Hii1. - rewrite /eq_op /= eq_refl /= eq_sym. by move: Hlt; rewrite ltn_neqAle => /andP[]. rewrite (tpermD Hu Hu1); apply/andP; split; first last. by apply/nandP => /=; left; rewrite eq_sym. case/altP: (inord i =P v) => Hv. subst v; rewrite eltrL Hii1. by apply (leq_trans Hlt). case/altP: (inord i.+1 =P v) => Hv1. subst v; rewrite eltrR. by move: Hlt; rewrite Hii1 ltnS ltn_neqAle eq_sym Hu /=. by rewrite eltrD. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition