proposition: Lemma lattice_finite_sup3P x y: finite_set x -> nonempty x -> sub x E -> (gle r (supremum r x) y <-> (forall z, inc z x -> gle r z y)).
proof: Proof. move=> fsx nex xsr. have hs:= (lattice_finite_sup2 fsx nex xsr). have or: order r by case:lr. move: (supremum_pr or xsr hs) => [[p1 p2] p3]; split. move=> p4 z zx; move: (p2 _ zx) => p5; order_tac. move=> p4; apply: p3; split => //. move: nex=> [u ux]; move: (p4 _ ux) => p5; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)