proposition: Lemma finite_subset_lattice_inf r X: lattice r -> finite_set X -> nonempty X -> sub X (substrate r) -> exists x, greatest_lower_bound r X x.
proof: Proof. move=> [or lr];apply: finite_set_induction3. + by move=>a b asr bsr; move: (lr _ _ asr bsr)=> [p1 p2]. + move=> a b x y asr bsr. move /(glbP or asr)=> [[xsr lb] glex]. have st: sub (a +s1 b) (substrate r) by apply: setU1_sub. have sd: sub (doubleton x b) (substrate r) by apply: sub_set2. move=> /(glbP or sd) [[ysr lby] lgley]. have xy := (lby _ (set2_1 x b)). have lbyy:= (lby _ (set2_2 x b)). apply /(glbP or st); split. split =>// z /setU1_P; case; last by move=> ->. move=>za; move: (lb _ za)=> xa; order_tac. move=> z [ze xx]. apply: lgley; split=>//; move=> t /set2_P [] ->. apply: glex; split=>//. move=> u ua; apply: xx; fprops. apply: xx; fprops. + by move=> Z x Zr _ /(glbP or Zr) [[xsr _] _]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)