proposition: Lemma sub_list_ok : forall l k n i, k < length l -> k+n <= length l -> i < n -> element_at (sub_list l k n) i = element_at l (k+i).
proof: Proof. intros l k n. functional induction (sub_list l k n); simpl; intros. refl. lia. destruct i. refl. apply IHl0; try lia. apply IHl0; lia. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)