proposition: Lemma lattice_finite_inf3P x y: finite_set x -> nonempty x -> sub x E -> (gle r y (infimum r x) <-> (forall z, inc z x -> gle r y z)).
proof: Proof. move=> fsx nex xsr. have hs:= (lattice_finite_inf2 fsx nex xsr). have or: order r by move: lr => [ok _]. have [[p1 p2] p3] := (infimum_pr or xsr hs). split; first by 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)