generalize ub, lb, etc. from reals.v

- replace `pred` with `set` in `reals.v` and propagate
- replace `-' E` by `-%R @' E`

theories/Rstruct.v

@@ -374,44 +374,45 @@ Canonical R_rcfType := RcfType R Rreal_closed_axiom.
 End ssreal_struct.
 
 Local Open Scope ring_scope.
-Require Import reals boolp.
+Require Import reals boolp classical_sets.
 
 Section ssreal_struct_contd.
 
-Lemma is_upper_boundE (E : pred R) x : is_upper_bound E x = (x \in ub E).
+Lemma is_upper_boundE (E : set R) x : is_upper_bound E x = ((ub E) x).
 Proof.
-rewrite /is_upper_bound inE forallbE asboolE /=; apply/eq_forall=> y.
-by rewrite -(reflect_eq implyP) (reflect_eq (RleP _ _)).
+apply/eq_forall=> y.
+by rewrite propeqE; split => h Ey; [apply/RleP/h|apply/RleP/h].
 Qed.
 
-Lemma boundE (E : pred R) : bound E = has_ub E.
+Lemma boundE (E : set R) : bound E = has_ub E.
 Proof. by apply/eq_exists=> x; rewrite is_upper_boundE. Qed.
 
-Lemma completeness' (E : pred R) : has_sup E -> {m : R | is_lub E m}.
+Lemma completeness' (E : set R) : has_sup E -> {m : R | is_lub E m}.
 Proof. by move=> [eE bE]; rewrite -boundE in bE; apply: completeness. Qed.
 
-Definition real_sup (E : pred R) : R :=
+Definition real_sup (E : set R) : R :=
   if pselect (has_sup E) isn't left hsE then 0 else projT1 (completeness' hsE).
 
-Lemma real_sup_is_lub (E : pred R) : has_sup E -> is_lub E (real_sup E).
+Lemma real_sup_is_lub (E : set R) : has_sup E -> is_lub E (real_sup E).
 Proof.
 by move=> hsE; rewrite /real_sup; case: pselect=> // ?; case: completeness'.
 Qed.
 
-Lemma real_sup_ub (E : pred R) : has_sup E -> real_sup E \in ub E.
+Lemma real_sup_ub (E : set R) : has_sup E -> (ub E) (real_sup E).
 Proof. by move=> /real_sup_is_lub []; rewrite is_upper_boundE. Qed.
 
-Lemma real_sup_out (E : pred R) : ~ has_sup E -> real_sup E = 0.
+Lemma real_sup_out (E : set R) : ~ has_sup E -> real_sup E = 0.
 Proof. by move=> nosup; rewrite /real_sup; case: pselect. Qed.
 
 (* :TODO: rewrite like this using (a fork of?) Coquelicot *)
 (* Lemma real_sup_adherent (E : pred R) : real_sup E \in closure E. *)
-Lemma real_sup_adherent (E : pred R) (eps : R) :
+Lemma real_sup_adherent (E : set R) (eps : R) :
   has_sup E -> 0 < eps -> exists2 e : R, E e & (real_sup E - eps) < e.
 Proof.
 move=> supE eps_gt0; set m := _ - eps; apply: contrapT=> mNsmall.
-have: m \in ub E.
-  apply/ubP=> y Ey; have /negP := mNsmall (ex_intro2 _ _ y Ey _).
+have: (ub E) m.
+  move=> y Ey.
+  have /negP := mNsmall (ex_intro2 _ _ y Ey _).
   by rewrite -leNgt.
 have [_ /(_ m)] := real_sup_is_lub supE.
 rewrite is_upper_boundE => m_big /m_big /RleP.

theories/altreals/distr.v

@@ -157,8 +157,8 @@ Qed.
 Local Lemma isd3 : psum mu <= 1.
 Proof.
 rewrite psumE; [apply/isd1 | apply/isd2 | apply/sup_le_ub].
-  by exists 0; apply/imsetbP; exists fset0; rewrite big_fset0.
-apply/ubP=> y /imsetbP[x ->]; rewrite big_fset_seq /=.
+  by exists 0, fset0; rewrite big_fset0.
+apply/ubP=> y [x ->]; rewrite big_fset_seq /=.
 by case: isd => _; apply; case: x => x /= /canonical_uniq.
 Qed.
 

theories/altreals/realseq.v

@@ -7,6 +7,7 @@
 From mathcomp Require Import all_ssreflect all_algebra.
 Require Import mathcomp.bigenough.bigenough.
 Require Import xfinmap boolp ereal reals discrete.
+Require Import classical_sets.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -213,7 +214,7 @@ Proof. by move=> le_uv; apply/(@ncvg_le_from 0). Qed.
 Lemma ncvg_nbounded u x : ncvg u x%:E -> nbounded u.
 Proof.                   (* FIXME: factor out `sup` of a finite set *)
 case/(_ (B x 1)) => K cu; pose S := [seq `|u n| | n <- iota 0 K].
-pose M : R := sup [pred x in S]; pose e := Num.max (`|x| + 1) (M + 1).
+pose M : R := sup [set x : R | x \in S]; pose e := Num.max (`|x| + 1) (M + 1).
 apply/asboolP/nboundedP; exists e => [|n]; first by rewrite ltxU ltr_paddl.
 case: (ltnP n K); last first.
   move/cu; rewrite inE eclamp_id ?ltr01 // => ltunBx1.
@@ -534,18 +535,18 @@ Qed.
 Lemma nlim_sup (u : nat -> R) l :
     (forall n m, (n <= m)%N -> u n <= u m)
   -> ncvg u l%:E
-  -> sup [pred r | `[exists n, r == u n]] = l.
+  -> sup [set r | exists n, r = u n] = l.
 Proof.
 move=> mn_u cv_ul; set S := (X in sup X); suff: ncvg u (sup S)%:E.
   by move/nlimE; move/nlimE: cv_ul => -> [->].
 elim/nbh_finW=> /= e gt0_e; have sS: has_sup S.
   apply/has_supP; split; first exists (u 0%N).
-    by apply/imsetbP; exists 0%N.
-  exists l; apply/ubP => _ /imsetbP[n ->].
+    by exists 0%N.
+  exists l; apply/ubP => _ [n ->].
   by rewrite -lee_fin; apply/ncvg_homo_le.
-have /sup_adherent := sS => /(_ _ gt0_e) [r /imsetbP] [N ->] lt_uN.
+have /sup_adherent := sS => /(_ _ gt0_e) [r] [N ->] lt_uN.
 exists N => n le_Nn; rewrite !inE distrC ger0_norm ?subr_ge0.
-  by apply/sup_upper_bound => //; apply/imsetbP; exists n.
+  by apply/sup_upper_bound => //; exists n.
 by rewrite ltr_subl_addr -ltr_subl_addl (lt_le_trans lt_uN) ?mn_u.
 Qed.