diff options
Diffstat (limited to 'contrib/setoid_ring/Ring_theory.v')
| -rw-r--r-- | contrib/setoid_ring/Ring_theory.v | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/contrib/setoid_ring/Ring_theory.v b/contrib/setoid_ring/Ring_theory.v index caa704595..cefdcf52b 100644 --- a/contrib/setoid_ring/Ring_theory.v +++ b/contrib/setoid_ring/Ring_theory.v @@ -59,8 +59,7 @@ Section Power. induction j;simpl. rewrite IHj. rewrite (mul_comm x (pow_pos x j *pow_pos x j)). - set (w:= x*pow_pos x j);unfold w at 2. - rewrite (mul_comm x (pow_pos x j));unfold w. + setoid_rewrite (mul_comm x (pow_pos x j)) at 2. repeat rewrite mul_assoc. apply (Seq_refl _ _ Rsth). repeat rewrite mul_assoc. apply (Seq_refl _ _ Rsth). apply (Seq_refl _ _ Rsth). |