proposition: Lemma initialSeg_nth : forall (l: list A) size x, x < size -> nth_error (initialSeg l size) x = nth_error l x.
proof: Proof. induction l; intros size x x_size. destruct size; trivial. destruct size; simpl. lia. destruct x; simpl. trivial. apply IHl. auto with arith. Qed.
imports: Coq(Permutation Setoid) CoLoR(NatUtil LogicUtil)