proposition: Lemma lattice_finite_sup5 f: (Hf f) -> inc (sup_graph r f) (substrate r).
proof: Proof. move: (proj1 lr) => or [fgf fsd ned srf]. have aux: (has_sup_graph r f). apply: lattice_finite_sup2 => //;first by apply: finite_range. move: ned => [x xd]; exists (Vg f x); fprops. by move: (sup_graph_pr1 or srf aux) => /(lubP or srf) [[pa _] _]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)