proposition: Lemma change_nth_correct : forall {T} n m (l : list T) d f, ((n < length l)%nat /\ n = m /\ nth n (change_nth m l f) d = f (nth n l d)) \/ nth n (change_nth m l f) d = nth n l d.
proof: Proof. intros T n m l d f. revert n m. induction l as [|h l IH]. intros n m. now right. intros [|n] [|m] ; simpl. - left. repeat split. apply Nat.lt_0_succ. - now right. - now right. - destruct (IH n m) as [[H1 [H2 H3]]|H]. 2: now right. left. repeat split. now rewrite <-Nat.succ_lt_mono. now rewrite <- H2. exact H3. 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