proposition: Lemma finalSeg_nth_idx : forall l i j a, nth_error (finalSeg l i) j = Some a -> length l > i + j.
proof: Proof. induction l; unfold finalSeg; intros. destruct i; destruct j; inversion H. destruct i. destruct j. simpl; lia. simpl in *; rewrite initialSeg_full in H; auto with arith. set (w := nth_some l j H); lia. simpl in * . assert (length l > i + j). apply IHl with a0; trivial. lia. Qed.
imports: Coq(Permutation Setoid) CoLoR(NatUtil LogicUtil)