fact: Definition compact_ (I : interval) : CProp := match I with | realline => False | openr b => False | openl a => False | closer b => False | closel a => False | olor a b => False | olcr a b => False | clor a b => False | clcr a b => a [<=] b end.
imports: CoRN.ftc.NthDerivative