equal
deleted
inserted
replaced
141 also have "\<dots> = c * (\<parallel>x\<parallel> * inverse \<parallel>x\<parallel>)" |
141 also have "\<dots> = c * (\<parallel>x\<parallel> * inverse \<parallel>x\<parallel>)" |
142 by (rule Groups.mult_assoc) |
142 by (rule Groups.mult_assoc) |
143 also |
143 also |
144 from gt have "\<parallel>x\<parallel> \<noteq> 0" by simp |
144 from gt have "\<parallel>x\<parallel> \<noteq> 0" by simp |
145 then have "\<parallel>x\<parallel> * inverse \<parallel>x\<parallel> = 1" by simp |
145 then have "\<parallel>x\<parallel> * inverse \<parallel>x\<parallel> = 1" by simp |
146 also have "c * 1 \<le> b" by (simp add: b_def le_maxI1) |
146 also have "c * 1 \<le> b" by (simp add: b_def) |
147 finally show "y \<le> b" . |
147 finally show "y \<le> b" . |
148 qed |
148 qed |
149 qed |
149 qed |
150 then show ?thesis .. |
150 then show ?thesis .. |
151 qed |
151 qed |