proposition: Lemma another_sym h p : another h p = another p h.
proof: Proof. rewrite /another; congr odflt; apply eq_pick => ?; by rewrite andbC. 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