proposition: Lemma nth_finalSeg_nth: forall l k p, nth_error (finalSeg l k) p = nth_error l (k + p).
proof: Proof. intros l k; revert l. induction k; intros; simpl. rewrite finalSeg_full; trivial. destruct l. destruct p; trivial. rewrite <- IHk; trivial. Qed.
imports: Coq(Permutation Setoid) CoLoR(NatUtil LogicUtil)