proposition: Lemma ocitvD : semi_setD_closed ocitv.
proof: Proof. move=> _ _ [a _ <-] /ocitvP[|[b ltb]] ->. rewrite setD0; exists [set `]a.1, a.2]%classic]. by split=> [//|? ->//||? ? -> ->//]; rewrite bigcup_set1. rewrite setDE setCitv/= setIUr -!set_itvI. rewrite /Order.meet/= /Order.meet/= /Order.join/= ?(andbF, orbF)/= ?(meetEtotal, joinEtotal). rewrite -negb_or le_total/=; set c := minr _ _; set d := maxr _ _. have inside : a.1 < c -> d < a.2 -> `]a.1, c] `&` `]d, a.2] = set0. rewrite -subset0 lt_minr lt_maxl => /andP[a12 ab1] /andP[_ ba2] x /= []. have b1a2 : b.1 <= a.2 by rewrite ltW// (lt_trans ltb). have a1b2 : a.1 <= b.2 by rewrite ltW// (lt_trans _ ltb). rewrite /c /d (min_idPr _)// (max_idPr _)// !in_itv /=. move=> /andP[a1x xb1] /andP[b2x xa2]. by have := lt_le_trans b2x xb1; case: ltgtP ltb. exists ((if a.1 < c then [set `]a.1, c]%classic] else set0) `|` (if d < a.2 then [set `]d, a.2]%classic] else set0)); split. - by rewrite finite_setU; do! case: ifP. - by move=> ? []; case: ifP => ? // ->//=. - by rewrite bigcup_setU; congr (_ `|` _); case: ifPn => ?; rewrite ?bigcup_set1 ?bigcup_set0// set_itv_ge. - move=> I J/=; case: ifP => //= ac; case: ifP => //= da [] // -> []// ->. by rewrite inside// => -[]. by rewrite setIC inside// => -[]. 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