src/HOL/Probability/Probability_Mass_Function.thy

     using assms \<open>R x y\<close> by (auto simp: quotient_def dest: equivp_symp equivp_transp)
   with eq show "measure p {x. R x y} = measure q {y. R x y}"
     by auto
 qed
 
-bnf pmf: "'a pmf" map: map_pmf sets: set_pmf bd : "natLeq" rel: rel_pmf
+bnf pmf: "'a pmf" map: map_pmf sets: set_pmf bd : "card_suc natLeq" rel: rel_pmf
 proof -
   show "map_pmf id = id" by (rule map_pmf_id)
   show "\<And>f g. map_pmf (f \<circ> g) = map_pmf f \<circ> map_pmf g" by (rule map_pmf_compose)
   show "\<And>f g::'a \<Rightarrow> 'b. \<And>p. (\<And>x. x \<in> set_pmf p \<Longrightarrow> f x = g x) \<Longrightarrow> map_pmf f p = map_pmf g p"
     by (intro map_pmf_cong refl)
 
   show "\<And>f::'a \<Rightarrow> 'b. set_pmf \<circ> map_pmf f = (`) f \<circ> set_pmf"
     by (rule pmf_set_map)
 
-  show "(card_of (set_pmf p), natLeq) \<in> ordLeq" for p :: "'s pmf"
+  show "card_order (card_suc natLeq)" using natLeq_card_order by (rule card_order_card_suc)
+  show "BNF_Cardinal_Arithmetic.cinfinite (card_suc natLeq)"
+    using natLeq_Cinfinite natLeq_card_order Cinfinite_card_suc by blast
+  show "regularCard (card_suc natLeq)" using natLeq_card_order natLeq_Cinfinite
+    by (rule regular_card_suc)
+
+  show "(card_of (set_pmf p), card_suc natLeq) \<in> ordLess" for p :: "'s pmf"
   proof -
     have "(card_of (set_pmf p), card_of (UNIV :: nat set)) \<in> ordLeq"
       by (rule card_of_ordLeqI[where f="to_nat_on (set_pmf p)"])
          (auto intro: countable_set_pmf)
     also have "(card_of (UNIV :: nat set), natLeq) \<in> ordLeq"
       by (metis Field_natLeq card_of_least natLeq_Well_order)
-    finally show ?thesis .
+    finally show ?thesis using card_suc_greater natLeq_card_order ordLeq_ordLess_trans by blast
   qed
 
   show "\<And>R. rel_pmf R = (\<lambda>x y. \<exists>z. set_pmf z \<subseteq> {(x, y). R x y} \<and>
     map_pmf fst z = x \<and> map_pmf snd z = y)"
      by (auto simp add: fun_eq_iff rel_pmf.simps)

       qed (simp add: pr_def map_bind_pmf split_beta map_pmf_def[symmetric] p map_pmf_comp)
     }
     then show ?thesis
       by(auto simp add: le_fun_def)
   qed
-qed (fact natLeq_card_order natLeq_cinfinite)+
+qed
 
 lemma map_pmf_idI: "(\<And>x. x \<in> set_pmf p \<Longrightarrow> f x = x) \<Longrightarrow> map_pmf f p = p"
 by(simp cong: pmf.map_cong)
 
 lemma rel_pmf_conj[simp]: