equal
deleted
inserted
replaced
471 { |
471 { |
472 assume eq: "n = n'" |
472 assume eq: "n = n'" |
473 then have ?case using 4 |
473 then have ?case using 4 |
474 apply (cases "p +\<^sub>p p' = 0\<^sub>p") |
474 apply (cases "p +\<^sub>p p' = 0\<^sub>p") |
475 apply (auto simp add: Let_def) |
475 apply (auto simp add: Let_def) |
476 apply blast |
|
477 done |
476 done |
478 } |
477 } |
479 ultimately have ?case by blast |
478 ultimately have ?case by blast |
480 } |
479 } |
481 ultimately show ?case by blast |
480 ultimately show ?case by blast |