fact: Fixpoint domain_ind' (d : domain) : P d := match d return P d with | Never => P_Never | Always => P_Always | Partial d e => P_Partial d e | Derivable n k f le => P_Derivable n k f le | Derivable2 m n k f le => P_Derivable2 m n k f le | Continuous n e => P_Continuous n e | Continuous2 m n e => P_Continuous2 m n e | Integrable f e1 e2 => P_Integrable f e1 e2 | ParamIntegrable n f e1 e2 => P_ParamIntegrable n f e1 e2 | LocallyParamIntegrable n f e => P_LocallyParamIntegrable n f e | And ld => P_And ld ((fix domain_ind'' (ld : seq domain) : foldr (fun d acc => P d /\ acc) True ld := match ld return foldr (fun d acc => P d /\ acc) True ld with | nil => I | cons h q => conj (domain_ind' h) (domain_ind'' q) end) ld) | Forall e1 e2 d => P_Forall e1 e2 d (domain_ind' d) | Forone e d => P_Forone e d (domain_ind' d) | Locally n d => P_Locally n d (domain_ind' d) | Locally2 m n d => P_Locally2 m n d (domain_ind' d) | ForallWide n e1 e2 d => P_ForallWide n e1 e2 d (domain_ind' d) end.
imports: Coq(Reals Datatypes ssreflect ssrbool) mathcomp(seq) Rcomplements Hierarchy Derive RInt RInt_analysis Derive_2d Continuity ElemFct