proposition: Lemma interp_domain_set_nth : forall n l b, interp_domain (set_nth 0 l n (nth 0 l n)) b <-> interp_domain l b.
proof: Proof. intros n l b. split ; apply interp_domain_ext => k. rewrite nth_set_nth /=. case ssrnat.eqnP. intros H. now apply f_equal. easy. 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