proposition: Lemma interp_set_nth : forall n l e, interp (set_nth 0 l n (nth 0 l n)) e = interp l e.
proof: Proof. intros n l e. apply interp_ext. intros k. rewrite nth_set_nth /=. case ssrnat.eqnP. intros H. now apply f_equal. easy. Qed.
imports: Coq(Reals Datatypes ssreflect ssrbool) mathcomp(seq) Rcomplements Hierarchy Derive RInt RInt_analysis Derive_2d Continuity ElemFct