From 8eb6370b94af56b94d2645aa4eaab5915341b961 Mon Sep 17 00:00:00 2001 From: Russell O'Connor Date: Thu, 29 Jun 2017 19:56:34 -0400 Subject: Fix Zmod_div. --- theories/ZArith/Zdiv.v | 1 + 1 file changed, 1 insertion(+) (limited to 'theories') 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. -- cgit v1.2.3