proposition: Lemma Exercise4_7c: has_least r.
proof: Proof. move: (finite_set_minimal1 (@sub_refl (substrate r)) nes). move=> [x xsr xp]; exists x;split => // u usr. move: (lattice_inf_pr lr xsr usr)=> [p1 p2 p3]. move: lr => [or _]. have isr:inc (inf r x u) (substrate r) by order_tac. by move: (xp _ isr p1) => aux; rewrite aux in p2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)