proposition: Lemma initialSeg_length : forall (l: list A) size, length (initialSeg l size) = min size (length l).
proof: Proof. induction l; intro size. destruct size; trivial. destruct size; simpl. trivial. rewrite IHl; trivial. Qed.
imports: Coq(Permutation Setoid) CoLoR(NatUtil LogicUtil)