proposition: Lemma finalSeg_copy : forall l el k n, k <= n -> finalSeg (copy n el ++ l) k = copy (n - k) el ++ l.
proof: Proof. induction k; intros. rewrite finalSeg_full. replace (n - 0) with n; [trivial | lia]. destruct n. lia. unfold finalSeg; simpl. fold (finalSeg (copy n el ++ l) k). rewrite IHk; trivial. lia. Qed.
imports: Coq(Permutation Setoid) CoLoR(NatUtil LogicUtil)