proposition: Lemma auto_derive_helper : forall (e : expr) l n, let '(a,b) := D e n in interp_domain l (simplify_domain b) -> is_derive (fun x => interp (set_nth R0 l n x) e) (nth R0 l n) (interp l a).
proof: Proof. intros e l n. generalize (D_correct e l n). destruct (D e n) as (d1,d2). intros H1 H2. apply H1. now apply simplify_domain_correct. Qed.
imports: Coq(Reals Datatypes ssreflect ssrbool) mathcomp(seq) Rcomplements Hierarchy Derive RInt RInt_analysis Derive_2d Continuity ElemFct