proposition: Lemma initialSeg_full : forall l n, n >= length l -> initialSeg l n = l.
proof: Proof. induction l. destruct n; trivial. simpl. intros n n_l. destruct n. lia. simpl. rewrite IHl; trivial. auto with arith. Qed.
imports: Coq(Permutation Setoid) CoLoR(NatUtil LogicUtil)