proposition: Lemma drop_nth_insert_nth : forall l p el, length l >= p -> drop_nth (insert_nth l p el) p = l.
proof: Proof. induction l; simpl; intros. destruct p; trivial. lia. destruct p. unfold insert_nth; simpl. rewrite finalSeg_full. unfold drop_nth; simpl. rewrite finalSeg_cons; trivial. change (drop_nth (insert_nth (a::l) (S p) el) (S p)) with (a :: drop_nth (insert_nth l p el) p). rewrite IHl; trivial. lia. Qed.
imports: Coq(Permutation Setoid) CoLoR(NatUtil LogicUtil)