proposition: Lemma finalSeg_empty : forall l k, k >= length l -> finalSeg l k = nil.
proof: Proof. induction l. destruct k; trivial. intros k k_al. destruct k. simpl in k_al. lia. unfold finalSeg; simpl. fold (finalSeg l k). apply IHl. simpl in k_al. lia. Qed.
imports: Coq(Permutation Setoid) CoLoR(NatUtil LogicUtil)