proposition: Lemma is_ocitv a b : ocitv `]a, b]%classic.
proof: Proof. by exists (a, b); split => //=; rewrite in_itv/= andbT. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum ssrint interval) mathcomp(finmap fingroup perm rat) HB(structures) mathcomp.classical(mathcomp_extra boolp classical_sets) mathcomp.classical(functions fsbigop cardinality) reals ereal signed topology numfun normedtype sequences esum real_interval measure realfun