fact: Definition add_to_nth i x (ls : list Z) : list Z := update_nth i (fun y => x + y) ls.
imports: Coq.ZArith.ZArith Coq.Lists.List Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.QArith.QArith_base Coq.QArith.Qreduction Coq.QArith.Qround