proposition: Lemma ex5m_prop4: inc (ex5m J k x) (Vg (psE S) k).
proof: Proof. move: (proj1 mp2) => kI; rewrite -(sEr kI). exact: (inc_infimum_substrate (proj1 (lEr kI)) (ex5m_prop1) (ex5m_prop2)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)