proposition: Lemma uniform_unfold_pair {M : probMonad real_realType} def (P : rel X) : uniform (def, def) (cp (enum X) (enum X)) >>= (fun hp => Ret (P hp.1 hp.2)) = Ret (P a a) <|(/ 9)%coqR%:pr|> (Ret (P a b) <|(/ 8)%coqR%:pr|> (Ret (P a c) <|(/ 7)%coqR%:pr|> (Ret (P b a) <|(/ 6)%coqR%:pr|> (Ret (P b b) <|(/ 5)%coqR%:pr|> (Ret (P b c) <|(/ 4)%coqR%:pr|> (Ret (P c a) <|(/ 3)%coqR%:pr|> (Ret (P c b) <|(/ 2)%coqR%:pr|> Ret (P c c)))))))) :> M _.
proof: Proof. rewrite [LHS](_ : _ = fmap (uncurry P) (uniform (def, def) (cp (enum X) (enum X)))); last first. rewrite fmapE; bind_ext; by case. by rewrite -(compE (fmap _)) -(uniform_naturality _ true) enumE. Qed.
imports: Reals Lra mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra reals Rstruct) infotheo(ssrR realType_ext Reals_ext proba) monae_lib hierarchy monad_lib fail_lib proba_lib