proposition: Lemma rem_rcons2_inv (T:eqType) (a: T) l (s := take (index a l) l): rem a (rcons l a) = l -> a\notin s /\ l = s ++ nseq (size l - (index a l)) a.
proof: Proof. rewrite /s{s} => h; split. elim:l {h} => // b l Hr /=;case: ifP => //. by rewrite eq_sym in_cons negb_or Hr => ->. elim:l h => // b l IHl /=; case: eqP. move => ->; rewrite subn0 cat0s; clear IHl b; elim:l => // b l Hr /= [->]. by move/Hr ->. by move => nba [] /IHl; rewrite subSS cat_cons => <-. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)