785 apply (subgoal_tac "[uminus a, one] divides pmult qa qaa") |
785 apply (subgoal_tac "[uminus a, one] divides pmult qa qaa") |
786 apply (simp add: poly_primes del: pmult_Cons) |
786 apply (simp add: poly_primes del: pmult_Cons) |
787 apply (auto simp add: divides_def simp del: pmult_Cons) |
787 apply (auto simp add: divides_def simp del: pmult_Cons) |
788 apply (rule_tac x = qb in exI) |
788 apply (rule_tac x = qb in exI) |
789 apply (subgoal_tac "poly (pmult (pexp [uminus a, one] (order a p)) (pmult qa qaa)) = |
789 apply (subgoal_tac "poly (pmult (pexp [uminus a, one] (order a p)) (pmult qa qaa)) = |
790 poly (pmult (pexp [uminus a, one] (?order a p)) (pmult [uminus a, one] qb))") |
790 poly (pmult (pexp [uminus a, one] (order a p)) (pmult [uminus a, one] qb))") |
791 apply (drule poly_mult_left_cancel [THEN iffD1], force) |
791 apply (drule poly_mult_left_cancel [THEN iffD1], force) |
792 apply (subgoal_tac "poly (pmult (pexp [uminus a, one] (order a q)) |
792 apply (subgoal_tac "poly (pmult (pexp [uminus a, one] (order a q)) |
793 (pmult (pexp [uminus a, one] (order a p)) (pmult qa qaa))) = |
793 (pmult (pexp [uminus a, one] (order a p)) (pmult qa qaa))) = |
794 poly (pmult (pexp [uminus a, one] (order a q)) |
794 poly (pmult (pexp [uminus a, one] (order a q)) |
795 (pmult (pexp [uminus a, one] (order a p)) (pmult [uminus a, one] qb)))") |
795 (pmult (pexp [uminus a, one] (order a p)) (pmult [uminus a, one] qb)))") |