equal
deleted
inserted
replaced
567 by (subgoal_tac "#0<m" 1); |
567 by (subgoal_tac "#0<m" 1); |
568 by (rotate_tac ~1 1); |
568 by (rotate_tac ~1 1); |
569 by (asm_full_simp_tac (simpset() addsimps [int_0_le_mult_iff]) 1); |
569 by (asm_full_simp_tac (simpset() addsimps [int_0_le_mult_iff]) 1); |
570 by (subgoal_tac "m*k<m*#1" 1); |
570 by (subgoal_tac "m*k<m*#1" 1); |
571 by (dtac (zmult_zless_cancel1 RS iffD1) 1); |
571 by (dtac (zmult_zless_cancel1 RS iffD1) 1); |
572 by Auto_tac; |
572 by (auto_tac (claset(), simpset() addsimps [linorder_neq_iff])); |
573 qed "zcong_zless_0"; |
573 qed "zcong_zless_0"; |
574 |
574 |
575 Goal "#0<m ==> (EX! b. #0<=b & b<m & [a = b] (mod m))"; |
575 Goal "#0<m ==> (EX! b. #0<=b & b<m & [a = b] (mod m))"; |
576 by Auto_tac; |
576 by Auto_tac; |
577 by (subgoal_tac "[b = y] (mod m)" 2); |
577 by (subgoal_tac "[b = y] (mod m)" 2); |