1254 using np |
1254 using np |
1255 apply simp_all |
1255 apply simp_all |
1256 apply (case_tac n', simp, simp) |
1256 apply (case_tac n', simp, simp) |
1257 apply (case_tac n, simp, simp) |
1257 apply (case_tac n, simp, simp) |
1258 apply (case_tac n, case_tac n', simp add: Let_def) |
1258 apply (case_tac n, case_tac n', simp add: Let_def) |
1259 apply (case_tac "pa +\<^sub>p p' = 0\<^sub>p") |
1259 apply (auto simp add: polyadd_eq_const_degree)[2] |
1260 apply (auto simp add: polyadd_eq_const_degree) |
|
1261 apply (metis head_nz) |
1260 apply (metis head_nz) |
1262 apply (metis head_nz) |
1261 apply (metis head_nz) |
1263 apply (metis degree.simps(9) gr0_conv_Suc head.simps(1) less_Suc0 not_less_eq) |
1262 apply (metis degree.simps(9) gr0_conv_Suc head.simps(1) less_Suc0 not_less_eq) |
1264 apply (metis degree.simps(9) gr0_conv_Suc nat_less_le order_le_less_trans) |
|
1265 done |
1263 done |
1266 |
1264 |
1267 lemma polymul_head_polyeq: |
1265 lemma polymul_head_polyeq: |
1268 assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" |
1266 assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" |
1269 shows "\<lbrakk>isnpolyh p n0; isnpolyh q n1 ; p \<noteq> 0\<^sub>p ; q \<noteq> 0\<^sub>p \<rbrakk> \<Longrightarrow> head (p *\<^sub>p q) = head p *\<^sub>p head q" |
1267 shows "\<lbrakk>isnpolyh p n0; isnpolyh q n1 ; p \<noteq> 0\<^sub>p ; q \<noteq> 0\<^sub>p \<rbrakk> \<Longrightarrow> head (p *\<^sub>p q) = head p *\<^sub>p head q" |