equal
deleted
inserted
replaced
733 show "0 < (1::nat)" by simp |
733 show "0 < (1::nat)" by simp |
734 show "i \<le> j ==> k + i \<le> k + j" by simp |
734 show "i \<le> j ==> k + i \<le> k + j" by simp |
735 show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: mult_less_mono2) |
735 show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: mult_less_mono2) |
736 qed |
736 qed |
737 |
737 |
|
738 instance nat :: no_zero_divisors |
|
739 proof |
|
740 fix a::nat and b::nat show "a ~= 0 \<Longrightarrow> b ~= 0 \<Longrightarrow> a * b ~= 0" by auto |
|
741 qed |
|
742 |
738 lemma nat_mult_1: "(1::nat) * n = n" |
743 lemma nat_mult_1: "(1::nat) * n = n" |
739 by simp |
744 by simp |
740 |
745 |
741 lemma nat_mult_1_right: "n * (1::nat) = n" |
746 lemma nat_mult_1_right: "n * (1::nat) = n" |
742 by simp |
747 by simp |