proposition: Lemma bij_same_r { F1 F2 : finType } { w0 : F1 } { w0' : F2 } { f : F1 -> F2 } ( bij_f : bijective f ) : @r F1 w0 = @r F2 w0'.
proof: Proof. unfold r. f_equal. f_equal. f_equal. erewrite <- on_card_preimset with (f := f). 2:{ destruct bij_f as [g hfg hgf]. exists g. - intros x hx. apply hfg. - intros x hx. apply hgf. } rewrite cardsT. reflexivity. Qed.
imports: 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 UniformDistrLemmas Prelude choice_type StateTransformingLaxMorph RulesStateProb)