fact: Definition totally_bounded (P : IR -> CProp) : CProp := {x : IR | P x} and (forall e, [0] [<] e -> {l : list IR | forall x, member x l -> P x | forall x, P x -> {y : IR | member y l | AbsSmall e (x[-]y)}}).
imports: CoRN.algebra.CSetoidInc CoRN.reals.RealLists