equal
deleted
inserted
replaced
566 apply auto |
566 apply auto |
567 apply (case_tac xa) |
567 apply (case_tac xa) |
568 apply auto |
568 apply auto |
569 apply (case_tac xa) |
569 apply (case_tac xa) |
570 apply auto |
570 apply auto |
571 apply (auto simp add: finite_M_bounded_by_nat) |
|
572 done |
571 done |
573 |
572 |
574 lemma card_less_Suc: |
573 lemma card_less_Suc: |
575 assumes zero_in_M: "0 \<in> M" |
574 assumes zero_in_M: "0 \<in> M" |
576 shows "Suc (card {k. Suc k \<in> M \<and> k < i}) = card {k \<in> M. k < Suc i}" |
575 shows "Suc (card {k. Suc k \<in> M \<and> k < i}) = card {k \<in> M. k < Suc i}" |