proposition: Lemma initialSeg_copy : forall el n k, initialSeg (copy n el) k = copy (min n k) el.
proof: Proof. induction n; destruct k; intros; simpl; trivial. rewrite IHn; trivial. Qed.
imports: Coq(Permutation Setoid) CoLoR(NatUtil LogicUtil)