proposition: Lemma bijective_isdistr { F : finType} { w0 : F } {f : F -> F} (Hbij : bijective f) : isdistr (@f_dprod F w0 f).
proof: Proof. rewrite /f_dprod. split. move => [w1 w2]. - destruct (f (w1, w2).1 == (w1, w2).2) eqn: Heq; rewrite Heq. -- exact r_nonneg. -- trivial. - move => J uniq_J. apply: le_trans. apply: (gen_cardinality_bound J uniq_J _). -- move => [t1 t2] /=. destruct (f t1 == t2) eqn:Heq; auto. exact r_nonneg. -- rewrite sum_prod_bij. rewrite sumr_const /r -GRing.invf_div GRing.divr1 GRing.mulVf. auto. exact (@card_non_zero F w0). by move => w; exact r_nonneg. 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)