proposition: Lemma initialSeg_app : forall l l' n, n <= length l -> initialSeg (l ++ l') n = initialSeg l n.
proof: Proof. induction l; intros. destruct n; simpl; trivial. simpl in H; lia. destruct n; simpl; trivial. rewrite (IHl l' n); trivial. simpl in H; lia. Qed.
imports: Coq(Permutation Setoid) CoLoR(NatUtil LogicUtil)