equal
deleted
inserted
replaced
289 qed "nat_cmult_eq_mult"; |
289 qed "nat_cmult_eq_mult"; |
290 |
290 |
291 Goal "Card(n) ==> 2 |*| n = n |+| n"; |
291 Goal "Card(n) ==> 2 |*| n = n |+| n"; |
292 by (asm_simp_tac |
292 by (asm_simp_tac |
293 (simpset() addsimps [cmult_succ_lemma, Card_is_Ord, |
293 (simpset() addsimps [cmult_succ_lemma, Card_is_Ord, |
294 read_instantiate [("j","0")] cadd_commute]) 1); |
294 inst "j" "0" cadd_commute]) 1); |
295 qed "cmult_2"; |
295 qed "cmult_2"; |
296 |
296 |
297 |
297 |
298 val sum_lepoll_prod = [sum_eq_2_times RS equalityD1 RS subset_imp_lepoll, |
298 val sum_lepoll_prod = [sum_eq_2_times RS equalityD1 RS subset_imp_lepoll, |
299 asm_rl, lepoll_refl] MRS (prod_lepoll_mono RSN (2, lepoll_trans)) |
299 asm_rl, lepoll_refl] MRS (prod_lepoll_mono RSN (2, lepoll_trans)) |