proposition: Lemma insert_nth_permut: forall (l: list A) el n, permutation eqA_dec (insert_nth l n el) (el::l).
proof: Proof. induction l; intros. unfold insert_nth, finalSeg; destruct n; simpl; apply permut_refl. destruct n; unfold insert_nth; simpl. rewrite finalSeg_full; apply permut_refl. unfold finalSeg; simpl. fold (finalSeg l n); fold (insert_nth l n el). apply permut_tran with (a :: el :: l). apply permut_cons. apply IHl. change (el :: a :: l) with ((el :: nil) ++ a :: l). change (a :: el :: l) with (a :: (el :: nil) ++ l). apply permut_middle. Qed.
imports: Coq(Setoid Morphisms Basics) CoLoR(ListExtras NatUtil LogicUtil)