proposition: Lemma sampleFsq_support { F : finType} { w0 : F } {a1 a2 : F} {f : F -> F} (f_bij : bijective f) (H : 0 < (@sampleFsq_f F w0 f f_bij) (a1, a2)) : f a1 == a2.
proof: Proof. simpl in H. rewrite /f_dprod /= in H. case (f a1 == a2) eqn:Heq; auto. by rewrite ltxx in H. 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)