proposition: Lemma length_change_nth : forall {T} n (l : list T) f, length (change_nth n l f) = length l.
proof: Proof. intros T n l f. revert n. induction l as [|h l IH]. easy. intros [|n]. easy. simpl. apply f_equal, IH. Qed.
imports: Coq(Bool Reals) Flocq(Zaux Raux) Coq(List) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect) Stdlib Coquelicot Xreal Xreal_derive Basic Interval Interval_compl Taylor_model Tree Prog