proposition: Lemma list_middle_inv : forall n l, n < length l -> exists l1 x l2, l = l1++x::l2 /\ length l1 = n.
proof: Proof. Proof using. intros. gen l. induction n; introv N; destruct l as [|x l']; rew_list in *; try solve [ false; math ]. { exists~ (@nil A) x l'. } { forwards (l1&x'&l2&E&M): IHn l'. math. exists (x::l1) x' l2. subst l'. rew_list~. } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)