equal
deleted
inserted
replaced
125 "\<not> x * x + y * y < 0" |
125 "\<not> x * x + y * y < 0" |
126 by (simp add: not_less sum_squares_ge_zero) |
126 by (simp add: not_less sum_squares_ge_zero) |
127 |
127 |
128 lemma sum_squares_eq_zero_iff: |
128 lemma sum_squares_eq_zero_iff: |
129 "x * x + y * y = 0 \<longleftrightarrow> x = 0 \<and> y = 0" |
129 "x * x + y * y = 0 \<longleftrightarrow> x = 0 \<and> y = 0" |
130 by (simp add: sum_nonneg_eq_zero_iff) |
130 by (simp add: add_nonneg_eq_0_iff) |
131 |
131 |
132 lemma sum_squares_le_zero_iff: |
132 lemma sum_squares_le_zero_iff: |
133 "x * x + y * y \<le> 0 \<longleftrightarrow> x = 0 \<and> y = 0" |
133 "x * x + y * y \<le> 0 \<longleftrightarrow> x = 0 \<and> y = 0" |
134 by (simp add: le_less not_sum_squares_lt_zero sum_squares_eq_zero_iff) |
134 by (simp add: le_less not_sum_squares_lt_zero sum_squares_eq_zero_iff) |
135 |
135 |