diff -r 7f229b0212fe -r 3d40cf74726c src/HOL/BNF_Cardinal_Arithmetic.thy
--- a/src/HOL/BNF_Cardinal_Arithmetic.thy	Mon Mar 03 03:13:45 2014 +0100
+++ b/src/HOL/BNF_Cardinal_Arithmetic.thy	Mon Mar 03 12:48:19 2014 +0100
@@ -199,7 +199,7 @@
   "Cinfinite r1 \<or> Cinfinite r2 \<Longrightarrow> Cinfinite (r1 +c r2)"
 unfolding cinfinite_def csum_def by (rule conjI[OF _ card_of_Card_order]) (auto simp: Field_card_of)
 
-lemma Cinfinite_csum_strong:
+lemma Cinfinite_csum_weak:
   "\<lbrakk>Cinfinite r1; Cinfinite r2\<rbrakk> \<Longrightarrow> Cinfinite (r1 +c r2)"
 by (erule Cinfinite_csum1)
 
@@ -335,6 +335,9 @@
 lemma cprod_mono2: "p2 \<le>o r2 \<Longrightarrow> q *c p2 \<le>o q *c r2"
 by (simp only: cprod_def ordLeq_Times_mono2)
 
+lemma cprod_mono: "\<lbrakk>p1 \<le>o r1; p2 \<le>o r2\<rbrakk> \<Longrightarrow> p1 *c p2 \<le>o r1 *c r2"
+by (rule ordLeq_transitive[OF cprod_mono1 cprod_mono2])
+
 lemma ordLeq_cprod2: "\<lbrakk>Cnotzero p1; Card_order p2\<rbrakk> \<Longrightarrow> p2 \<le>o p1 *c p2"
 unfolding cprod_def by (rule Card_order_Times2) (auto intro: czeroI)
 
@@ -347,6 +350,15 @@
 lemma Cinfinite_cprod2: "\<lbrakk>Cnotzero r1; Cinfinite r2\<rbrakk> \<Longrightarrow> Cinfinite (r1 *c r2)"
 by (blast intro: cinfinite_cprod2 Card_order_cprod)
 
+lemma cprod_cong: "\<lbrakk>p1 =o r1; p2 =o r2\<rbrakk> \<Longrightarrow> p1 *c p2 =o r1 *c r2"
+by (metis cprod_mono ordIso_iff_ordLeq)
+
+lemma cprod_cong1: "\<lbrakk>p1 =o r1\<rbrakk> \<Longrightarrow> p1 *c p2 =o r1 *c p2"
+by (metis cprod_mono1 ordIso_iff_ordLeq)
+
+lemma cprod_cong2: "p2 =o r2 \<Longrightarrow> q *c p2 =o q *c r2"
+by (metis cprod_mono2 ordIso_iff_ordLeq)
+
 lemma cprod_com: "p1 *c p2 =o p2 *c p1"
 by (simp only: cprod_def card_of_Times_commute)
 
@@ -514,6 +526,9 @@
 unfolding cinfinite_def cprod_def
 by (rule Card_order_Times_infinite[THEN conjunct1]) (blast intro: czeroI)+
 
+lemma cprod_infinite: "Cinfinite r \<Longrightarrow> r *c r =o r"
+using cprod_infinite1' Cinfinite_Cnotzero ordLeq_refl by blast
+
 lemma cexp_cprod_ordLeq:
   assumes r1: "Card_order r1" and r2: "Cinfinite r2"
   and r3: "Cnotzero r3" "r3 \<le>o r2"