proposition: Lemma perm_eq_iperm (A : eqType) (a b : seq A) : perm_eq a b -> iperm a = iperm b :> M _.
proof: Proof. have [n na] := ubnP (size a); elim: n a na b => // n ih a na b. case: a na => [na|a1 a2]; first by move=> /perm_size/esym/size0nil ->. rewrite [in X in X -> _]/= ltnS => na. case: b => [/perm_size //|b1 b2]. have [a1b1|a1b1 ab] := eqVneq a1 b1. by rewrite {}a1b1 perm_cons => ab /=; rewrite (ih _ na b2). have [b21 [b22 Hb]] : exists b21 b22, b2 = rcons b21 a1 ++ b22. apply: mem_rcons_cat. by move/perm_mem : ab => /(_ a1); rewrite mem_head inE (negbTE a1b1). have {} : perm_eq a2 (b1 :: b21 ++ b22). move: ab; rewrite Hb -cats1 -catA -cat_cons perm_sym. by rewrite perm_catCA perm_cons perm_sym. by move=> /(ih _ na) /= ->; rewrite Hb iperm_insert. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib Equations(Equations)