equal
deleted
inserted
replaced
378 assumes "x * y \<le> 0" and "\<not> y \<le> 0" and "\<not> x \<le> 0" |
378 assumes "x * y \<le> 0" and "\<not> y \<le> 0" and "\<not> x \<le> 0" |
379 shows False |
379 shows False |
380 using assms by (metis mult_le_0_iff) |
380 using assms by (metis mult_le_0_iff) |
381 |
381 |
382 |
382 |
383 subsection {* Linear arithmetic for natural numbers *} |
383 subsection \<open>Linear arithmetic for natural numbers\<close> |
384 |
384 |
385 declare [[smt_nat_as_int]] |
385 declare [[smt_nat_as_int]] |
386 |
386 |
387 lemma "2 * (x::nat) \<noteq> 1" by smt |
387 lemma "2 * (x::nat) \<noteq> 1" by smt |
388 |
388 |