proposition: Lemma reflection_nonsense : forall (Z : eqType) (a x : Z), (a == x) = true -> a = x.
proof: Proof. intros Z a x. intro Hax. unshelve eapply elimT. exact (a == x). apply eqP. assumption. Qed.
imports: Mon(FiniteProbabilities SPropMonadicStructures SpecificationMonads MonadExamples SPropBase FiniteProbabilities) Coq(RelationClasses Morphisms) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples Commutativity) mathcomp(all_ssreflect all_algebra reals distr realsum) Crypt(Axioms ChoiceAsOrd only_prob.SubDistr)