proposition: Lemma interp_AppExt_set_nth_not_const : forall k f le l n x, interp (set_nth 0 l n x) (AppExt k f le) = apply k f (foldr (fun v acc i => if ssrnat.eqn i v then interp (set_nth 0 l n x) (nth (Cst 0) le v) else acc i) (nth 0 (map (interp l) le)) (index_not_const le n)).
proof: Proof. intros k f le l n x. simpl. apply apply_ext => m _. generalize (index_not_const_correct n le m). induction (index_not_const le n) as [|t s IHs]. simpl => Hp. case (ssrnat.leqP (size le) m) => Hs. rewrite 2?nth_default ?size_map //. rewrite 2?(nth_map (Cst 0)) //. rewrite (is_const_correct _ n _ l x (nth 0 l n)). apply interp_set_nth. now apply Hp. rewrite (@in_cons ssrnat_eqType) /= -ssrnat.eqnE. case E: (ssrnat.eqn m t). intros _. rewrite (ssrnat.eqnP E). case (ssrnat.leqP (size le) t) => Hs. now rewrite 2?nth_default ?size_map. now rewrite (nth_map (Cst 0)). simpl. apply IHs. Qed.
imports: Coq(Reals Datatypes ssreflect ssrbool) mathcomp(seq) Rcomplements Hierarchy Derive RInt RInt_analysis Derive_2d Continuity ElemFct