proposition: Lemma iperm_cons_splits (A : eqType) (s : seq A) p : iperm (p :: s) = splits s >>= (fun '(ys, zs) => liftM2 (fun x y => x ++ p :: y) (iperm ys) (iperm zs)) :> M _.
proof: Proof. have [n ns] := ubnP (size s); elim: n s ns => // n ih s ns. move: s ns => [ns |h t]. by rewrite /= bindretf insertE bindretf /= /liftM2 /= !bindretf. rewrite [in X in X -> _]/= ltnS => ns. rewrite [in RHS]/= bindA. under eq_bind do rewrite alt_bindDl 2!bindretf. transitivity (iperm [:: h, p & t] : M _). by apply: perm_eq_iperm; rewrite -cat1s -(cat1s h) perm_catCA. rewrite [p :: t]lock /= -lock ih // bindA; bind_ext => -[a b] /=. rewrite liftM2E /liftM2 /= bindA -alt_bindDr; bind_ext => a'. rewrite bindA (plus_commute (insert h a'))// -alt_bindDr. by under eq_bind do rewrite insert_cat. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib Equations(Equations)