proposition: Lemma initialFinalSeg_length : forall l k, length (initialSeg l k) + length (finalSeg l k) = length l.
proof: Proof. intros. rewrite initialSeg_length, finalSeg_length. destruct (Compare_dec.le_gt_dec k (length l)); solve [rewrite min_l; lia | rewrite min_r; lia]. Qed.
imports: Coq(Permutation Setoid) CoLoR(NatUtil LogicUtil)