proposition: Lemma ex5m_prop3_bis i: inc i J -> gle (Vg Er k) (ex5m J k x) (ex5_M i k (Vg x i)).
proof: Proof. move: (proj1 mp2) => kI. move:(ex5m_prop4); rewrite - (sEr kI) => /(proj42 (proj1 (lEr kI))). move/(ex5m_prop3); apply. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)