proposition: Lemma sumr_const (T : finType) (x : R): \sum_(i <- enum T) x = x * (#|T|%:~R).
proof: Proof. rewrite sum_const_seq_finType. 2: { apply enum_uniq. } rewrite GRing.sumr_const pmulrn /=. rewrite !enumT. unfold intmul. rewrite GRing.mulrC. rewrite GRing.Theory.mulr_natl. apply f_equal. rewrite card_seq_sub. + rewrite cardE. rewrite -enumT. reflexivity. + rewrite -enumT. apply enum_uniq. 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)