proposition: Lemma finalSeg_app_right : forall (l: list A) k n, n > length l -> finalSeg (l ++ k) n = finalSeg k (n - length l).
proof: Proof. induction l; intros. simpl; replace (n - 0) with n; [trivial | lia]. destruct n. lia. unfold finalSeg; simpl. fold (finalSeg (l ++ k) n). rewrite (IHl k n). unfold finalSeg; trivial. simpl in H; lia. Qed.
imports: Coq(Permutation Setoid) CoLoR(NatUtil LogicUtil)