proposition: Lemma joins_le J (r : seq J) (P : {pred J}) (F : J -> L) (u : L) : (forall x : J, P x -> F x <= u) -> \join_(x <- r | P x) F x <= u.
proof: Proof. by move=> leFm; elim/big_rec: _ => // i x Px xu; rewrite leUx leFm. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)