diff options
| author | Anton Trunov | 2019-05-29 15:37:31 +0300 |
|---|---|---|
| committer | Anton Trunov | 2019-05-29 15:37:31 +0300 |
| commit | e9c284b97b76e214f417ccc33907853bc0b8aa8e (patch) | |
| tree | b7a8df4adad80129e1f1ffab4308dba17816744d /mathcomp/algebra | |
| parent | 42db44ce8df9f24d90c321d57e81e2d5bf83bd48 (diff) | |
incorporate new suggestions by @CohenCyril
Diffstat (limited to 'mathcomp/algebra')
| -rw-r--r-- | mathcomp/algebra/polydiv.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/algebra/polydiv.v b/mathcomp/algebra/polydiv.v index 2ac2c3e..b65742d 100644 --- a/mathcomp/algebra/polydiv.v +++ b/mathcomp/algebra/polydiv.v @@ -2238,7 +2238,7 @@ Proof. apply/eqP/idP=> [d0|]; last first. case/or3P; [by move/eqP->; rewrite div0p| by move/eqP->; rewrite divp0|]. by move/divp_small. -case: (eqVneq p 0) => [->//|pn0]; case: (eqVneq q 0) => [->//| qn0]. +case: eqVneq => // _; case: eqVneq => // qn0. move: (divp_eq p q); rewrite d0 mul0r add0r. move/(f_equal (fun x : {poly R} => size x)). by rewrite size_scale ?lc_expn_scalp_neq0 // => ->; rewrite ltn_modp qn0 !orbT. |