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