proposition: Lemma length_sub_list : forall l k n, k < length l -> k+n <= length l -> length (sub_list l k n) = n.
proof: Proof. intros l k n. functional induction (sub_list l k n); simpl; intros. lia. lia. destruct l'. simpl in *. lia. rewrite IHl0; simpl in *; lia. rewrite IHl0; lia. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)