proposition: Lemma finalSeg_nth_nth : forall l k p, p >= k -> nth_error l p = nth_error (finalSeg l k) (p - k).
proof: Proof. intros. rewrite nth_finalSeg_nth. replace (k + (p - k)) with p; trivial. lia. Qed.
imports: Coq(Permutation Setoid) CoLoR(NatUtil LogicUtil)