diff -r 22d1c5f2b9f4 -r 0dd3ac5fdbaa src/HOL/BNF_Cardinal_Arithmetic.thy
--- a/src/HOL/BNF_Cardinal_Arithmetic.thy	Mon Jun 27 15:54:18 2022 +0200
+++ b/src/HOL/BNF_Cardinal_Arithmetic.thy	Mon Jun 27 17:36:26 2022 +0200
@@ -817,24 +817,15 @@
 lemma Cinfinite_card_suc: "\<lbrakk> Cinfinite r ; card_order r \<rbrakk> \<Longrightarrow> Cinfinite (card_suc r)"
   using Cinfinite_cong[OF cardSuc_ordIso_card_suc Cinfinite_cardSuc] .
 
+lemma card_suc_least: "\<lbrakk>card_order r; Card_order s; r <o s\<rbrakk> \<Longrightarrow> card_suc r \<le>o s"
+  by (rule ordIso_ordLeq_trans[OF ordIso_symmetric[OF cardSuc_ordIso_card_suc]])
+    (auto intro!: cardSuc_least simp: card_order_on_Card_order)
+
 lemma regularCard_cardSuc: "Cinfinite k \<Longrightarrow> regularCard (cardSuc k)"
   by (rule infinite_cardSuc_regularCard) (auto simp: cinfinite_def)
 
-lemma regular_card_suc: "card_order r \<Longrightarrow> Cinfinite r \<Longrightarrow> regularCard (card_suc r)"
+lemma regularCard_card_suc: "card_order r \<Longrightarrow> Cinfinite r \<Longrightarrow> regularCard (card_suc r)"
   using cardSuc_ordIso_card_suc Cinfinite_cardSuc regularCard_cardSuc regularCard_ordIso
   by blast
 
-(* card_suc (natLeq +c |UNIV| ) *)
-
-lemma card_order_card_suc_natLeq_UNIV: "card_order (card_suc (natLeq +c |UNIV :: 'a set| ))"
-  using card_order_card_suc card_order_csum natLeq_card_order card_of_card_order_on by blast
-
-lemma cinfinite_card_suc_natLeq_UNIV: "cinfinite (card_suc (natLeq +c |UNIV :: 'a set| ))"
-  using Cinfinite_card_suc card_order_csum natLeq_card_order card_of_card_order_on natLeq_Cinfinite
-      Cinfinite_csum1 by blast
-
-lemma regularCard_card_suc_natLeq_UNIV: "regularCard (card_suc (natLeq +c |UNIV :: 'a set| ))"
-  using regular_card_suc card_order_csum natLeq_card_order card_of_card_order_on Cinfinite_csum1
-      natLeq_Cinfinite by blast
-
 end