proposition: Lemma cardinality_bound {T : finType} (J : seq T) (Huniq: uniq J) (k : R) (k_geq0 : 0 <= k) : \sum_(j <- J) k <= (#|T|%:~R) * k.
proof: Proof. rewrite GRing.mulrC. rewrite sum_const_seq_finType. 2: { exact Huniq. } rewrite GRing.sumr_const pmulrn /=. have hfoo' : k *~ #|seq_sub_finType (T:=T) J| = k * #|seq_sub_finType (T:=T) J|%:~R. { by rewrite mulrzr. } rewrite hfoo' /=. apply: ler_pmul; auto. - rewrite ler0z. rewrite lez_nat. reflexivity. - rewrite card_seq_sub. 2: eauto. rewrite cardT. rewrite ler_int. rewrite lez_nat. rewrite uniq_leq_size. 1,2: auto. intros x hx. 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)