fact: Definition Derive_Rn n (f : Rn n R) p g := Derive (fun x => apply n f (fun i => if ssrnat.eqn i p then x else g i)) (g p).
imports: Coq(Reals Datatypes ssreflect ssrbool) mathcomp(seq) Rcomplements Hierarchy Derive RInt RInt_analysis Derive_2d Continuity ElemFct