proposition: Lemma Exercise4_7i1 x: sub x (substrate r) -> has_infimum r x.
proof: Proof. move: Exercise4_7b => or xr; case: (emptyset_dichot x) => nex. move: (the_greatest_pr or Exercise4_7c1) => tlp. rewrite nex; exists (the_greatest r). rewrite glb_set0 //. by apply: (lattice_finite_inf2 lr (sub_finite_set xr fs) nex xr). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)