diff options
| -rw-r--r-- | theories/ZArith/Zdiv.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v index 140d1b3c8..54ab227e8 100644 --- a/theories/ZArith/Zdiv.v +++ b/theories/ZArith/Zdiv.v @@ -510,6 +510,7 @@ Qed. Lemma Zmod_div : forall a b, a mod b / b = 0. Proof. + intros a b. zero_or_not b. auto using Z.mod_div. Qed. |