proposition: Lemma sum_const_seq_finType { T : finType } ( J : seq T) (k : R) (Huniq : uniq J) : \sum_(j <- J) k = \sum_(j in (seq_sub_finType J)) k.
proof: Proof. rewrite /seq_sub_finType. simpl. rewrite big_const. rewrite big_const_seq. rewrite card_seq_sub. - simpl. rewrite count_predT. reflexivity. - apply Huniq. 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)