proposition: Lemma mem_permutations s t : (t \in permutations s) = perm_eq t s.
proof: Proof. have{s} [n [bs [-> Dn /permPr<- _]]] := permsP s. elim: n => [|n IHn] /= in t bs Dn *. by rewrite inE (nilP Dn); apply/eqP/perm_nilP. rewrite -[bs in tseq bs]cats0 in Dn *; have x0 : T by case: (tseq _) Dn. rewrite -[RHS](@andb_idl (last x0 t \in tseq bs)); last first. case/lastP: t {IHn} => [|t x] Dt; first by rewrite -(perm_size Dt) in Dn. by rewrite -[bs]cats0 -(perm_mem Dt) last_rcons mem_rcons mem_head. elim: bs [::] => [|[x [|m]] bs IHbs] //= bs2 in Dn *. rewrite cons_permsE -!cat_cons !mem_cat (mem_nseq m.+1) orbC andb_orl. rewrite {}IHbs ?(perm_size (perm_tseq bsCA)) //= (permPr (perm_tseq bsCA)). congr (_ || _); apply/mapP/andP=> [[t1 Dt1 ->] | [/eqP]]. by rewrite last_rcons perm_rcons perm_cons IHn in Dt1 *. case/lastP: t => [_ /perm_size//|t y]; rewrite last_rcons perm_rcons => ->. by rewrite perm_cons; exists t; rewrite ?IHn. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)