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