proposition: Lemma nth_insert_nth : forall l p el, length l >= p -> nth_error (insert_nth l p el) p = Some el.
proof: Proof. induction l; simpl; intros. destruct p; trivial. lia. destruct p; trivial. simpl. unfold finalSeg; simpl. fold (finalSeg l p); fold (insert_nth l p el). apply IHl. lia. Qed.
imports: Coq(Permutation Setoid) CoLoR(NatUtil LogicUtil)