proposition: Lemma gen_cardinality_bound : ∀ {T : finType} (J : seq T) (Huniq: uniq J) (π : T → R) (π_geq0 : ∀ t, 0 <= (π t)), \sum_(j <- J) (π j) <= \sum_(j <- enum T) (π j).
proof: Proof. intros T J hu π hπ. rewrite [X in _<=X](bigID [pred j : T | j \in J]) /=. rewrite ler_paddr ?sumr_ge0 // -[X in _<=X]big_filter. rewrite Order.POrderTheory.le_eqVlt; apply/orP; left; apply/eqP/perm_big. apply/uniq_perm; rewrite ?filter_uniq //; last move=> i. rewrite -enum_setT. apply enum_uniq. rewrite mem_filter; case/boolP: (_ \in _) => //=. intro. rewrite mem_enum. reflexivity. Qed.
imports: Coq(Relation_Definitions RelationClasses Morphisms Utf8) Mon(FiniteProbabilities SPropMonadicStructures SpecificationMonads MonadExamples SPropBase) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples Commutativity GenericRulesSimple) mathcomp(all_ssreflect all_algebra reals distr realsum) Crypt(Axioms ChoiceAsOrd SubDistr Couplings Theta_dens Theta_exCP LaxComp FreeProbProg)