equal
deleted
inserted
replaced
1510 |
1510 |
1511 lemma diffs0_imp_equal: "!!m::nat. [| m-n = 0; n-m = 0 |] ==> m=n" |
1511 lemma diffs0_imp_equal: "!!m::nat. [| m-n = 0; n-m = 0 |] ==> m=n" |
1512 by (simp split add: nat_diff_split) |
1512 by (simp split add: nat_diff_split) |
1513 |
1513 |
1514 lemma min_diff: "min (m - (i::nat)) (n - i) = min m n - i" |
1514 lemma min_diff: "min (m - (i::nat)) (n - i) = min m n - i" |
1515 unfolding min_def by auto |
1515 by auto |
1516 |
1516 |
1517 lemma inj_on_diff_nat: |
1517 lemma inj_on_diff_nat: |
1518 assumes k_le_n: "\<forall>n \<in> N. k \<le> (n::nat)" |
1518 assumes k_le_n: "\<forall>n \<in> N. k \<le> (n::nat)" |
1519 shows "inj_on (\<lambda>n. n - k) N" |
1519 shows "inj_on (\<lambda>n. n - k) N" |
1520 proof (rule inj_onI) |
1520 proof (rule inj_onI) |