This is the roadmap of the constructive proof of Lebesgue's dominated

This is the roadmap of the constructive proof of Lebesgue's dominated
convergence theorem in the order theoretic setting. I.e. we speak of
convergence (in terms of liminf and limsup) and not of norms/measures.

The formulation should be fully constructive:
 1. the exceeds relation is used in place of the derived negative notion
    <= for partial orders
 2. strong sup and infs are used in place of the weaker sup and infs
 3. the statement of Lebesgue's dominated converge theorem is just
    extensionality of the functional
      \lambda f. liminf f a_n
    with respect to the apartness relation # over real numbers and the
    exceeds/apartness relation over partial orders.

Interesting points to be noticed:
 a) one lemma used in the proof is Fatou. This lemma can be given in the
    usual negative formulation (i.e. on <=)
 b) another lemma used in the proof is that the liminf is less or equal to
    the limsup. This lemm can be given in the usual negative formulation
    (i.e. on <=). Moreover, we feel that if <= is not defined as
    ~< it is actually impossible to constructively prove it.