proposition: Lemma seg_tillEnd : forall l m n, n >= length l - m -> seg l m n = seg l m (length l - m).
proof: Proof. induction l. destruct m; destruct n; trivial. destruct m; destruct n; simpl; try solve [intro x; lia]. intro n_l; do 2 (rewrite initialSeg_full; [idtac | lia]); trivial. apply IHl. intro n_m; rewrite (IHl m (S n)); trivial. Qed.
imports: Coq(Permutation Setoid) CoLoR(NatUtil LogicUtil)