proposition: Lemma seg_nth : forall (l: list A) i j x, x < j -> nth_error (seg l i j) x = nth_error l (i + x).
proof: Proof. induction l. destruct i; destruct j; destruct x; trivial. intros i j x x_j. destruct i; simpl. destruct j; destruct x; simpl; try solve [lia | trivial]. change x at 2 with (0 + x). assert (xj: x < j). auto with arith. rewrite <- (IHl 0 j x xj); trivial. apply IHl; trivial. Qed.
imports: Coq(Permutation Setoid) CoLoR(NatUtil LogicUtil)