proposition: Lemma insert_nth_drop_nth : forall p l el, nth_error l p = Some el -> insert_nth (drop_nth l p) p el = l.
proof: Proof. induction p; intros. destruct l. inversion H. unfold drop_nth, insert_nth; simpl. rewrite finalSeg_cons, finalSeg_full. inversion H; trivial. destruct l. inversion H. unfold drop_nth, insert_nth; simpl. change (finalSeg (a::l) (S (S p))) with (finalSeg l (S p)). fold (drop_nth l p). change (finalSeg (a::drop_nth l p) (S p)) with (finalSeg (drop_nth l p) p). fold (insert_nth (drop_nth l p) p el). rewrite IHp; trivial. Qed.
imports: Coq(Permutation Setoid) CoLoR(NatUtil LogicUtil)