diff options
| author |  Russell O'Connor <roconnor@blockstream.io> | 2017-06-29 19:56:34 -0400 |
|---|---|---|
| committer | Russell O'Connor <roconnor@blockstream.io> | 2017-06-29 19:56:34 -0400 |
| commit | 8eb6370b94af56b94d2645aa4eaab5915341b961 (patch) | |
| tree | d221f1d5e3bc5ef2291f5f0f631aeb90dc6b79dc /theories | |
| parent | 79f2e62eb22318c9a2b0c96a19ef3fadd1ca781d (diff) | |
Fix Zmod_div.
Diffstat (limited to 'theories')
| -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. |