proposition: Lemma ex5m_prop3 y: (gle (Vg Er k) y (ex5m J k x) <-> (forall i, inc i J -> gle (Vg Er k) y (ex5_M i k (Vg x i)))).
proof: Proof. move:(proj1 mp2)(mp1) => jI [_ nej fsj]. have fs: finite_set (ex5_mij_J J k x) by apply: finite_fun_image. have ne:nonempty (ex5_mij_J J k x) by apply:funI_setne. apply: (iff_trans (lattice_finite_inf3P (lEr jI) y fs ne (ex5m_prop1))). split=> // hz z za. apply: hz; apply/funI_P; ex_tac. by move/funI_P: za => [i iJ ->]; apply: hz. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)