proposition: Lemma initialSeg_finalSeg_full : forall l k, initialSeg l k ++ finalSeg l k = l.
proof: Proof. intros l k; revert l; induction k. simpl; apply finalSeg_full. destruct l; trivial. unfold finalSeg; simpl. fold (finalSeg l k). rewrite IHk; trivial. Qed.
imports: Coq(Permutation Setoid) CoLoR(NatUtil LogicUtil)