proposition: Lemma update_nth_nil : forall {T} n f, update_nth n f (@nil T) = @nil T.
proof: Proof. destruct n; reflexivity. Qed.
imports: Coq.ZArith.ZArith Coq.Lists.List Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.QArith.QArith_base Coq.QArith.Qreduction Coq.QArith.Qround