proposition: Lemma has_sup_floor_set x : has_sup (floor_set x).
proof: Proof. split; [exists (- (Num.bound (-x))%:~R) | exists (Num.bound x)%:~R]. rewrite /floor_set/mkset rpredN rpred_int /= lerNl. case: (ger0P (-x)) => [/archi_boundP/ltW//|]. by move/ltW/le_trans; apply; rewrite ler0z. apply/ubP=> y /andP[_] /le_trans; apply. case: (ger0P x)=> [/archi_boundP/ltW|] //. by move/ltW/le_trans; apply; rewrite ler0z. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra) mathcomp(mathcomp_extra boolp classical_sets set_interval) Setoid