fact: Definition sig_forall_dec_T : Type := forall (P : nat -> Prop), (forall n, {P n} + {~P n}) -> {n | ~P n} + {forall n, P n}.
imports: QArith_base Qabs ConstructiveReals ConstructiveAbs ConstructiveLimits Logic.ConstructiveEpsilon