fact: Fixpoint expr_ind' (e : expr) : P e := match e return P e with | Var n => P_Var n | AppExt k f le => P_AppExt k f le ((fix expr_ind'' (le : seq expr) : foldr (fun e acc => P e /\ acc) True le := match le return foldr (fun e acc => P e /\ acc) True le with | nil => I | cons h q => conj (expr_ind' h) (expr_ind'' q) end) le) | AppExtD k f n le => P_AppExtD k f n le ((fix expr_ind'' (le : seq expr) : foldr (fun e acc => P e /\ acc) True le := match le return foldr (fun e acc => P e /\ acc) True le with | nil => I | cons h q => conj (expr_ind' h) (expr_ind'' q) end) le) | App e1 e2 => P_App e1 e2 (expr_ind' e1) (expr_ind' e2) | Subst e1 e2 => P_Subst e1 e2 (expr_ind' e1) (expr_ind' e2) | Cst r => P_Cst r | Binary o e1 e2 => P_Binary o e1 e2 (expr_ind' e1) (expr_ind' e2) | Unary o e => P_Unary o e (expr_ind' e) | Int f e1 e2 => P_Int f e1 e2 (expr_ind' f) (expr_ind' e1) (expr_ind' e2) end.
imports: Coq(Reals Datatypes ssreflect ssrbool) mathcomp(seq) Rcomplements Hierarchy Derive RInt RInt_analysis Derive_2d Continuity ElemFct