proposition: Lemma lattice_finite_sup4P f: (Hf f) -> forall y, (gle r(sup_graph r f) y <-> (forall z, inc z (domain f) -> gle r (Vg f z) y)).
proof: Proof. move => hf y. move:(lattice_finite_sup_aux hf) => [ne fr]. move: hf=> [fgf fsd ned srf];split. move /(lattice_finite_sup3P lr _ fr ne srf) => h z sd; apply: h; fprops. move=> h; apply /(lattice_finite_sup3P lr _ fr ne srf). by move=> z; move /(range_gP fgf) => [x xdf] ->; apply: h. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)