proposition: Lemma seg_exceeded l k n : n >= length l -> seg l k n = seg l k (length l).
proof: Proof. intro. rewrite seg_tillEnd, (@seg_tillEnd l k (length l)); trivial; lia. Qed.
imports: Coq(Permutation Setoid) CoLoR(NatUtil LogicUtil)