proposition: Lemma Exercise4_8u: infimum r emptyset = the_greatest r.
proof: Proof. move: Exercise4_7b => or. move: (the_greatest_pr or Exercise4_7c1) => tlp. have ok: (sub emptyset (substrate r)) by fprops. move: (infimum_pr1 or (Exercise4_7i1 ok)). rewrite (glb_set0) // => tlp1. by apply: (unique_greatest or). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)