proposition: Lemma joins_min_seq T (r : seq T) (P : {pred T}) (F : T -> L) (x : T) (l : L) : x \in r -> P x -> l <= F x -> l <= \join_(x <- r | P x) F x.
proof: Proof. by move=> ? ? /le_trans; apply; apply: joins_sup_seq. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)