diff options
Diffstat (limited to 'theories/ZArith/Zquot.v')
| -rw-r--r-- | theories/ZArith/Zquot.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/theories/ZArith/Zquot.v b/theories/ZArith/Zquot.v index b8b7808319..6b6ad7423c 100644 --- a/theories/ZArith/Zquot.v +++ b/theories/ZArith/Zquot.v @@ -462,7 +462,8 @@ Lemma Zrem_divides : forall a b, Zrem a b = 0 <-> exists c, a = b*c. Proof. intros. zero_or_not b. firstorder. - rewrite Z.rem_divide; trivial. split; intros (c,Hc); exists c; auto. + rewrite Z.rem_divide; trivial. + split; intros (c,Hc); exists c; subst; auto with zarith. Qed. (** Particular case : dividing by 2 is related with parity *) |