proposition: Lemma joins_min I (j : I) (l : L) (P : {pred I}) (F : I -> L) : P j -> l <= F j -> l <= \join_(i | P i) F i.
proof: Proof. exact: joins_min_seq. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)