proposition: Lemma lattice_finite_inf2 x: finite_set x -> nonempty x -> sub x E -> has_infimum r x.
proof: Proof. move:x;apply: finite_set_induction2. move => a asr;rewrite -/(singleton a). have ar: inc a (substrate r) by apply: asr; fprops. by move: lr => [or lr1]; move: (lr1 _ _ ar ar) =>[p1 p2]. move=> a b Hr nea ss. have p1: sub a (substrate r) by apply: sub_trans ss; fprops. have p2: inc b (substrate r) by apply: ss; fprops. have [c cs]:= (Hr nea p1). exists (inf r c b); apply: (lattice_finite_inf1 lr p1 cs p2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)